7 ms·

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 intractabl

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
- fmap 10y ago
  > 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. What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? Even if you can answer this, it sounds as if you are ignoring all the progress we have made in programming language design. The whole reason we have modern programming languages is to bridge the gap between the "informal proof" you keep in your head and an actual formal correctness proof. For example, C programs typically have a lot of bugs because there is such a large disconnect between the model of the program in your head (which also lacks most of the error states) and the actual state space of the program. Almost every abstraction in C is potentially leaky, and this just doesn't allow you to reason succinctly about your program. This is not even specific to C. The "simple" imperative programming models that are still used almost everywhere have exactly the same problem. The point of modern programming languages isn't that it's essentially the same thing, but with a scalable static analysis tacked on (types). The point is that we try to impose a discipline on programs which allows for modular correctness proofs. If you have a module implementing a certain data structure in ML, you can reason by parametricity about its correctness and once you have established whatever properties you want, nothing will every break them again. Essentially, you have just taken part of the state space and shrunk it down to a single bit. And that this is possible is not at all surprising! Everything you write, here or in your article, is also applicable to ordinary mathematics. So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions. We are making real progress in verification. Nowadays, there are scalable proof techniques for concurrent programs, even in the presence of weak memory models (GPS, iCAP, Iris, ...). There are compositional proof methods for program equivalence which scale to real programming languages (step-indexed logical relations, ...). There are language primitives for safe, efficient and easy to reason about concurrent and distributed programming (e.g., join calculus). And many, many more things which were previously thought of as stupendously complicated.
  - pron 10y ago
    > What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? A formal proof is one that can be mechanically translated to the logic's deduction rules. An informal proof is anything that is considered by mathematicians as proof, yet isn't a formal proof. It is smaller because it skips many details, but seems convincing enough. > it sounds as if you are ignoring all the progress we have made in programming language design We have not made significant progress when it comes to proving global logical properties, and I don't think anyone claims we have. There are languages that in theory can be used to prove correctness; in practice they have never been successfully used on real world programs, except for small and simplified ones, and even then with great effort by experts. > For example, C programs typically have a lot of bugs because... The reason why many languages are safer than C is because they prevent certain bugs by enforcing local properties, like memory safety. This is an example of a local property (that's easy to prove, even automatically, in many cases) that is known to be the cause of many costly bugs. Other languages don't fare significantly better when it comes to proving global correctness. The best we've done -- and that's not insignificant -- is reduce accidental complexity to proof. Like I show in my post, even a language with nothing but boolean variables and pure functions -- no memory allocation, no recursion or iteration of any kind and no higher-order functions -- where all programs are obviously terminating and the language is too weak to do anything useful, cannot be feasibly verified in general. Languages can help with local properties. The difficulty of proving logical correctness is dependent almost entirely on one thing: how simple your algorithm is. > The "simple" imperative programming models that are still used almost everywhere have exactly the same problem. So far imperative languages seem fare better than FP in terms of verification. Fully verifiable languages that are used for safety-critical realtime systems, are also imperative (although not in the same way JavaScript is). Make sure that by reading papers in PLT you're not falling into a bias trap. PLT nowadays is mostly concerned with FP, so papers will be on FP. Those who are interested in the verification aspects of PLT, will write about ideas that they think show promise. But most of verification research isn't PLT, and deals with imperative (or language-agnostic) algorithms, and they have their own results, which are no less promising. Neither has been able to "solve" verification in the sense people hoped in the 70s, and AFAIK, neither community is trying to do that. That doesn't stop them from publishing results that are very promising, but haven't been proven in practice yet. But if you're exposed to only one community, you may get the false sense that there is one consensus approach (there isn't), and we're slowly but surely getting to our destination (maybe we are, but we don't know for sure, and we don't know which approach works in practice). > for modular correctness proofs The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. Certain properties which could prevent certain bugs can definitely be made easier to prove with modularity -- they're local in some way -- but certainly not global logical correctness. Some people may hope that global correctness would turn out to be decomposable in enough use cases, but this is an empirical conjecture, with little proof so far. > Essentially, you have just taken part of the state space and shrunk it down to a single bit. Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't). The challenge is to figure out which properties that can prevent expensive bugs can be proved. > So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions. Theorems proven in math are much deeper yet deal with far simpler concepts than computer programs. The whole idea of computer programs is that they create small structures that defeat mathematical reasoning. It is no accident that Hilbert's program was laid to rest by the "discovery" of computer programs. Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. The best analogy is physics. The gravity equation is simple, modular, pure, equational, algebraic, composable -- whatever good PL adjective you may hope to assign. It is so simple that it is completely uninteresting to mathematicians. Yet, combine two of those equations together -- they compose very nicely -- and already no closed-form solution exists and the behavior can no longer be predicted; it is uninteresting to mathematicians (well, except for some instances), but for the opposite reasons. Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem. > We are making real progress in verification. Absolutely, but the goals are different. Most of the time we're talking local properties or a lot of effort or restricted domains. Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification. BTW, most progress in verification is not in PLT. Restricting yourself to PLT is a sure way to miss most of it.

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

fmap 10y ago
> 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. What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? Even if you can answer this, it sounds as if you are ignoring all the progress we have made in programming language design. The whole reason we have modern programming languages is to bridge the gap between the "informal proof" you keep in your head and an actual formal correctness proof. For example, C programs typically have a lot of bugs because there is such a large disconnect between the model of the program in your head (which also lacks most of the error states) and the actual state space of the program. Almost every abstraction in C is potentially leaky, and this just doesn't allow you to reason succinctly about your program. This is not even specific to C. The "simple" imperative programming models that are still used almost everywhere have exactly the same problem. The point of modern programming languages isn't that it's essentially the same thing, but with a scalable static analysis tacked on (types). The point is that we try to impose a discipline on programs which allows for modular correctness proofs. If you have a module implementing a certain data structure in ML, you can reason by parametricity about its correctness and once you have established whatever properties you want, nothing will every break them again. Essentially, you have just taken part of the state space and shrunk it down to a single bit. And that this is possible is not at all surprising! Everything you write, here or in your article, is also applicable to ordinary mathematics. So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions. We are making real progress in verification. Nowadays, there are scalable proof techniques for concurrent programs, even in the presence of weak memory models (GPS, iCAP, Iris, ...). There are compositional proof methods for program equivalence which scale to real programming languages (step-indexed logical relations, ...). There are language primitives for safe, efficient and easy to reason about concurrent and distributed programming (e.g., join calculus). And many, many more things which were previously thought of as stupendously complicated.
- pron 10y ago
  > What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? A formal proof is one that can be mechanically translated to the logic's deduction rules. An informal proof is anything that is considered by mathematicians as proof, yet isn't a formal proof. It is smaller because it skips many details, but seems convincing enough. > it sounds as if you are ignoring all the progress we have made in programming language design We have not made significant progress when it comes to proving global logical properties, and I don't think anyone claims we have. There are languages that in theory can be used to prove correctness; in practice they have never been successfully used on real world programs, except for small and simplified ones, and even then with great effort by experts. > For example, C programs typically have a lot of bugs because... The reason why many languages are safer than C is because they prevent certain bugs by enforcing local properties, like memory safety. This is an example of a local property (that's easy to prove, even automatically, in many cases) that is known to be the cause of many costly bugs. Other languages don't fare significantly better when it comes to proving global correctness. The best we've done -- and that's not insignificant -- is reduce accidental complexity to proof. Like I show in my post, even a language with nothing but boolean variables and pure functions -- no memory allocation, no recursion or iteration of any kind and no higher-order functions -- where all programs are obviously terminating and the language is too weak to do anything useful, cannot be feasibly verified in general. Languages can help with local properties. The difficulty of proving logical correctness is dependent almost entirely on one thing: how simple your algorithm is. > The "simple" imperative programming models that are still used almost everywhere have exactly the same problem. So far imperative languages seem fare better than FP in terms of verification. Fully verifiable languages that are used for safety-critical realtime systems, are also imperative (although not in the same way JavaScript is). Make sure that by reading papers in PLT you're not falling into a bias trap. PLT nowadays is mostly concerned with FP, so papers will be on FP. Those who are interested in the verification aspects of PLT, will write about ideas that they think show promise. But most of verification research isn't PLT, and deals with imperative (or language-agnostic) algorithms, and they have their own results, which are no less promising. Neither has been able to "solve" verification in the sense people hoped in the 70s, and AFAIK, neither community is trying to do that. That doesn't stop them from publishing results that are very promising, but haven't been proven in practice yet. But if you're exposed to only one community, you may get the false sense that there is one consensus approach (there isn't), and we're slowly but surely getting to our destination (maybe we are, but we don't know for sure, and we don't know which approach works in practice). > for modular correctness proofs The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. Certain properties which could prevent certain bugs can definitely be made easier to prove with modularity -- they're local in some way -- but certainly not global logical correctness. Some people may hope that global correctness would turn out to be decomposable in enough use cases, but this is an empirical conjecture, with little proof so far. > Essentially, you have just taken part of the state space and shrunk it down to a single bit. Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't). The challenge is to figure out which properties that can prevent expensive bugs can be proved. > So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions. Theorems proven in math are much deeper yet deal with far simpler concepts than computer programs. The whole idea of computer programs is that they create small structures that defeat mathematical reasoning. It is no accident that Hilbert's program was laid to rest by the "discovery" of computer programs. Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. The best analogy is physics. The gravity equation is simple, modular, pure, equational, algebraic, composable -- whatever good PL adjective you may hope to assign. It is so simple that it is completely uninteresting to mathematicians. Yet, combine two of those equations together -- they compose very nicely -- and already no closed-form solution exists and the behavior can no longer be predicted; it is uninteresting to mathematicians (well, except for some instances), but for the opposite reasons. Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem. > We are making real progress in verification. Absolutely, but the goals are different. Most of the time we're talking local properties or a lot of effort or restricted domains. Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification. BTW, most progress in verification is not in PLT. Restricting yourself to PLT is a sure way to miss most of it.