4 ms·

Let's consider an algorithm that shares state among multiple concurrent threads of execution without coordinating work through a lock. What is the probability

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.

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.