10 ms·

The focus on "totality" undersells one key advantage of the restrictions in this language. You gain the ability to easily prove general properties about your pr

The focus on "totality" undersells one key advantage of the restrictions in this language. You gain the ability to easily prove general properties about your program. This is not a consequence of totality. There are total programming languages which allow you to write programs with undecidable properties. This is really a language where properties are easy to prove, and termination happens to be one of them. The topic often comes up in the discussion of smart contracts on public blockchains, and people often get confused about what Rice's theorem says. I recently did a small write up on the topic (plug, plug) https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621#.heipbfzgf https://hackernoon.com/smart-contracts-turing-completeness-r...

pron 10y ago
Even if you restrict yourself to the weakest programming model possible -- finite state machines -- proving program correctness is still infeasible in general (PSPACE-complete for very simple FSM languages; EXPTIME or even 2-EXP for richer FSM languages, I think). It is a mistake to ignore all the results about FSM verification. In your post, you write: > However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward. This has been shown to be false in practice. The difficulty of proving real-world program correctness shows that real-world cases can get arbitrarily close to the worst-case predicted by the theory. Proving small programs like seL4 took required experts, and even then demanded an extreme simplification of all involved algorithms so that proof would be feasible. Even then, the cost was far beyond what any "ordinary" software could afford, and even after a great streamlining of the process and the use of "easily verifiable" languages, it is expected to be suitable only for resource-rich high-assurance software. Note that I'm not saying that formal methods are useless. I regularly use formal methods myself. But making them affordable is an art. I've written at length about the relevant theory here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
- murbard2 10y ago
  Thanks, those are good comments and I largely agree. I'll reply on a couple points though: 1) Yes, even in weak models, proving correctness is still intractable in general. However, this does not mean that a general algorithm has to be slow when run on typical instances. Typical instances are designed with a proof of correctness in mind, which is a strong indication that such a proof should be accessible. Unless you're generating programs randomy, programming generally entails carrying at least an informal proof of correctness in mind. 2) As you point out it is currently very hard and tedious to formalize those proofs. However, I believe this isn't a fundamental barrier. We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computations. Compare it to image recognition. It used to be very hard to do in software and it didn't work well. But when it finally started working, it didn't turn out to be particularly computer intensive. I think the same is true in formal verification. We don't know how to do it very well, but we're not up against theorems in complexity theory, we just lack the know-how.
  - pron 10y ago
    > this does not mean that a general algorithm has to be slow when run on typical instances True, but we have a few decades of experience with model checkers running on real programs. Yes, they work very well and are quite affordable, but their domain is rather specific (there is amazing work on model checkers designed to expand their domain and work on ever-larger programs, but the results aren't in yet). > Unless you're generating programs randomly, programming generally entails carrying at least an informal proof of correctness in mind. There are various results showing that the difference in size between an informal proof (even when correct, which, as experience shows often isn't[1]) and a formal one may be exponential. > We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Absolutely, but we must understand there are fundamental problems in play. > Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computation. This is unknown, but not very promising; certainly not promising enough to assume this will definitely be possible some day (let alone soon). See the result about symbolic model checking (basically the cost of proof that is allowed to exploit linguistic constructs) that I mention in my post. It turns out that in the general case (this time, we're not talking about completely "random" programs, but "random" programs that can be expressed succinctly in some language), it is as hard as a proof that doesn't exploit language, and the difficulty was found to hold in practice (the paper I quote calls it an "empirical fact"), i.e., real-world programs do get close to the worst-case. The goal of software verification nowadays isn't to find methods to verify general programs, but to find methods that catch a particular class of bugs (static analysis) or to prove arbitrary properties for specific domains or small programs (model checkers). The PLT approaches mostly focus on end-to-end verification, and don't currently attempt to make it affordable for "ordinary" programs. They're trying to make it as affordable as high-assurance testing (the kind done at NASA). In the seventies, the hope was that formal methods would one day allow us to prove arbitrary correctness properties of ordinary software. This is no longer the goal of the verification community today, despite the great achievements in some areas. [1]: Even when the informal proof is not just "in mind", but on paper, written by experts and peer reviewed: https://brooker.co.za/blog/2014/03/08/model-checking.html https://brooker.co.za/blog/2014/03/08/model-checking.html

pron 10y ago

Even if you restrict yourself to the weakest programming model possible -- finite state machines -- proving program correctness is still infeasible in general (PSPACE-complete for very simple FSM languages; EXPTIME or even 2-EXP for richer FSM languages, I think). It is a mistake to ignore all the results about FSM verification. In your post, you write: > However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward. This has been shown to be false in practice. The difficulty of proving real-world program correctness shows that real-world cases can get arbitrarily close to the worst-case predicted by the theory. Proving small programs like seL4 took required experts, and even then demanded an extreme simplification of all involved algorithms so that proof would be feasible. Even then, the cost was far beyond what any "ordinary" software could afford, and even after a great streamlining of the process and the use of "easily verifiable" languages, it is expected to be suitable only for resource-rich high-assurance software. Note that I'm not saying that formal methods are useless. I regularly use formal methods myself. But making them affordable is an art. I've written at length about the relevant theory here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

murbard2 10y ago
Thanks, those are good comments and I largely agree. I'll reply on a couple points though: 1) Yes, even in weak models, proving correctness is still intractable in general. However, this does not mean that a general algorithm has to be slow when run on typical instances. Typical instances are designed with a proof of correctness in mind, which is a strong indication that such a proof should be accessible. Unless you're generating programs randomy, programming generally entails carrying at least an informal proof of correctness in mind. 2) As you point out it is currently very hard and tedious to formalize those proofs. However, I believe this isn't a fundamental barrier. We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computations. Compare it to image recognition. It used to be very hard to do in software and it didn't work well. But when it finally started working, it didn't turn out to be particularly computer intensive. I think the same is true in formal verification. We don't know how to do it very well, but we're not up against theorems in complexity theory, we just lack the know-how.
- pron 10y ago
  > this does not mean that a general algorithm has to be slow when run on typical instances True, but we have a few decades of experience with model checkers running on real programs. Yes, they work very well and are quite affordable, but their domain is rather specific (there is amazing work on model checkers designed to expand their domain and work on ever-larger programs, but the results aren't in yet). > Unless you're generating programs randomly, programming generally entails carrying at least an informal proof of correctness in mind. There are various results showing that the difference in size between an informal proof (even when correct, which, as experience shows often isn't[1]) and a formal one may be exponential. > We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Absolutely, but we must understand there are fundamental problems in play. > Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computation. This is unknown, but not very promising; certainly not promising enough to assume this will definitely be possible some day (let alone soon). See the result about symbolic model checking (basically the cost of proof that is allowed to exploit linguistic constructs) that I mention in my post. It turns out that in the general case (this time, we're not talking about completely "random" programs, but "random" programs that can be expressed succinctly in some language), it is as hard as a proof that doesn't exploit language, and the difficulty was found to hold in practice (the paper I quote calls it an "empirical fact"), i.e., real-world programs do get close to the worst-case. The goal of software verification nowadays isn't to find methods to verify general programs, but to find methods that catch a particular class of bugs (static analysis) or to prove arbitrary properties for specific domains or small programs (model checkers). The PLT approaches mostly focus on end-to-end verification, and don't currently attempt to make it affordable for "ordinary" programs. They're trying to make it as affordable as high-assurance testing (the kind done at NASA). In the seventies, the hope was that formal methods would one day allow us to prove arbitrary correctness properties of ordinary software. This is no longer the goal of the verification community today, despite the great achievements in some areas. [1]: Even when the informal proof is not just "in mind", but on paper, written by experts and peer reviewed: https://brooker.co.za/blog/2014/03/08/model-checking.html https://brooker.co.za/blog/2014/03/08/model-checking.html