3 ms·

I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I won

I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I wonder if this: > This is useful because the language of types is much more concise than the language of terms. actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort? I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.

hopia 7y ago
In my experience it's much easier. A lot of my API relies on this. I even produce clients in other languages purely based on the API types which act as a form of specification. Haskell's compiler will generate all the logic for serialization and deserialization, leaving me to only implement the actual business logic.
- simiones 7y ago
  Serialization and deserialization are probably the lowest hanging fruit for this. Java has them, and it can even serialize objects with behavior. I think you're thinking of a very shallow kind of auto-generation of code, which doesn't include any kind of behavior beyond calling your API. The GP though was talking about generating the behavior based on the type specification, which is also doable in principle. For example, you could provide a complex type specification for a sorting function, and have the compiler infer the implementation. For example, you could declare a function which takes a list of `Ord a` and returns a list of `Ord a` such that the second list is a permutation of the first list and each element in the second list is <= to the next element (you of course need dependent types for this). With this type signature, the system could generate the code for a function which achieves this purpose. However, I do not believe that it will be easier to write that type signature (especially if you want to add properties like stability or time and space constraints) than it would be to write the actual sorting function yourself and sticking with `Ord a => [a] -> [a]`. I also don't think we will see anything like this in the near future that doesn't rely on a large set of pre-defined functions that the system simply fills in.
  - hopia 7y ago
    That was just a superficial example. If you include generics, template metaprogramming, auto derivations and such then you could achieve much more with code generation. My skills are just not advanced enough yet to fully utilize these in my programs.
agentultra 7y ago
Let's consider an algorithm that shares state among multiple concurrent threads of execution without coordinating work through a lock. What is the probability that an expert software engineer could write a correct implementation of this algorithm, I wonder? As their colleague will we be able to review that code and notice if it contains an error? What are the sufficient parameters for an acceptable solution: should it run with 8 threads and 2 state variables? I don't think we'll see these tools and practices become wide spread but I do see the cost of using them is coming down. I also see the number of cases where systems that aren't safety critical are never the less causing harm to property and people. It's possible that at this intersection we'll see the adoption grow: bringing down the cost of writing software that handles higher degrees of liability could be a useful tool to have.
- simiones 7y ago
  I'm not sure what you are refering to as "these techniques" - are you referring to full formal specification with dependent types? If so, then I think the answer so far is: even though few senior SEs could write correct implementations of that algorithm, there are definitely many more than the number of people who can write non-trivial software with complex dependent types in a decent amount of time. Of course, you can write code in Idris or Agda and be productive, but not if you want to do stuff like actually proving that your sort function produces a sorted permutation of original list and other similar somewhat rich tight bounds. The more you want to express in your types, the more complex your program becomes. A very nice example is how you would implement matrix multiplication in regular ways (with matrices of numbers) versus how much more work you need to add if you want to track physical quantities (with proper support for different physical quantities for each value in the matrix). It's easy to say {{1, 2}, {3, 4}} can be multiplied by {{5, 6}, {7, 8}}, but much harder to say if {{1m, 2kg}, {3N, 4Pa}} can be multiplied by {{5m, 6N}, {7Pa, 4kg}}.
  - agentultra 7y ago
    I think it's harder to find an error in a program than in a proof. At least for proofs that can be verified automatically by a computer. And that scales with the difficulty of the problem. A proof that a program copies files from one place to another is not interesting. However a proof that your algorithm can safely share state without a lock is. My point here is not that dependent type theory is going to take over the industry and we should all learn to write proofs! It's more that we can if we want to. Writing a proof with tactics in Lean feels a lot like programming with typed holes in Haskell (it's harder but the experience is similar). With training a motivated programmer can write proofs that verify their designs which provide a strong guarantee of correctness. Whether types are more expressive than programs... I think they are? That seems to be the whole point of Synquid: you can express complex constraints and proofs in your types that enable it to derive the program for you. Is that easier than simply writing the program? I think one should consider that writing the correct program is harder. And where getting it right matters a lot I hope that synthesis will one day allow us to derive those programs from their specifications (or at least the parts that matter the most). It would save a lot of the burden of proving that the program we wrote implements the specifications.

hopia 7y ago

In my experience it's much easier. A lot of my API relies on this. I even produce clients in other languages purely based on the API types which act as a form of specification. Haskell's compiler will generate all the logic for serialization and deserialization, leaving me to only implement the actual business logic.

simiones 7y ago
Serialization and deserialization are probably the lowest hanging fruit for this. Java has them, and it can even serialize objects with behavior. I think you're thinking of a very shallow kind of auto-generation of code, which doesn't include any kind of behavior beyond calling your API. The GP though was talking about generating the behavior based on the type specification, which is also doable in principle. For example, you could provide a complex type specification for a sorting function, and have the compiler infer the implementation. For example, you could declare a function which takes a list of `Ord a` and returns a list of `Ord a` such that the second list is a permutation of the first list and each element in the second list is <= to the next element (you of course need dependent types for this). With this type signature, the system could generate the code for a function which achieves this purpose. However, I do not believe that it will be easier to write that type signature (especially if you want to add properties like stability or time and space constraints) than it would be to write the actual sorting function yourself and sticking with `Ord a => [a] -> [a]`. I also don't think we will see anything like this in the near future that doesn't rely on a large set of pre-defined functions that the system simply fills in.
- hopia 7y ago
  That was just a superficial example. If you include generics, template metaprogramming, auto derivations and such then you could achieve much more with code generation. My skills are just not advanced enough yet to fully utilize these in my programs.

agentultra 7y ago

Let's consider an algorithm that shares state among multiple concurrent threads of execution without coordinating work through a lock. What is the probability that an expert software engineer could write a correct implementation of this algorithm, I wonder? As their colleague will we be able to review that code and notice if it contains an error? What are the sufficient parameters for an acceptable solution: should it run with 8 threads and 2 state variables? I don't think we'll see these tools and practices become wide spread but I do see the cost of using them is coming down. I also see the number of cases where systems that aren't safety critical are never the less causing harm to property and people. It's possible that at this intersection we'll see the adoption grow: bringing down the cost of writing software that handles higher degrees of liability could be a useful tool to have.

simiones 7y ago
I'm not sure what you are refering to as "these techniques" - are you referring to full formal specification with dependent types? If so, then I think the answer so far is: even though few senior SEs could write correct implementations of that algorithm, there are definitely many more than the number of people who can write non-trivial software with complex dependent types in a decent amount of time. Of course, you can write code in Idris or Agda and be productive, but not if you want to do stuff like actually proving that your sort function produces a sorted permutation of original list and other similar somewhat rich tight bounds. The more you want to express in your types, the more complex your program becomes. A very nice example is how you would implement matrix multiplication in regular ways (with matrices of numbers) versus how much more work you need to add if you want to track physical quantities (with proper support for different physical quantities for each value in the matrix). It's easy to say {{1, 2}, {3, 4}} can be multiplied by {{5, 6}, {7, 8}}, but much harder to say if {{1m, 2kg}, {3N, 4Pa}} can be multiplied by {{5m, 6N}, {7Pa, 4kg}}.
- agentultra 7y ago
  I think it's harder to find an error in a program than in a proof. At least for proofs that can be verified automatically by a computer. And that scales with the difficulty of the problem. A proof that a program copies files from one place to another is not interesting. However a proof that your algorithm can safely share state without a lock is. My point here is not that dependent type theory is going to take over the industry and we should all learn to write proofs! It's more that we can if we want to. Writing a proof with tactics in Lean feels a lot like programming with typed holes in Haskell (it's harder but the experience is similar). With training a motivated programmer can write proofs that verify their designs which provide a strong guarantee of correctness. Whether types are more expressive than programs... I think they are? That seems to be the whole point of Synquid: you can express complex constraints and proofs in your types that enable it to derive the program for you. Is that easier than simply writing the program? I think one should consider that writing the correct program is harder. And where getting it right matters a lot I hope that synthesis will one day allow us to derive those programs from their specifications (or at least the parts that matter the most). It would save a lot of the burden of proving that the program we wrote implements the specifications.