3 ms·

> 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 f

by 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.
- fmap 10y ago
  > The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. You are seriously overselling these results. Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates. > 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 point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction. > Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. You give an example of a termination problem which is equivalent to the consistency of ZFC. Does the consistency of ZFC "elude the power of math"? It's certainly a very simple question, much easier to write down than the Turing machine in question. > Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem. This applies to mathematics as well. You can write down simple sounding questions, like the Collatz conjecture you mention, which are actually extremely complicated. This is the point where complexity theory comes into the picture. For instance, I could generate random types in the calculus of constructions (random propositions) and ask if that type is inhabited (the proposition is provable). This is an undecidable problem and for complexity theoretic reason most instances (of a certain shape) will actually be hard. The concepts in programming aren't inherently more complicated than the concepts in mathematics. If anything, there are plenty of natural concepts in mathematics which behave far more chaotically than anything in CS (look at a table of homotopy groups of spheres and tell me where that pattern comes from). > 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. It's very much the goal for PLT. :) In practice, it's also very much in the future. Right now verifying large programs is possible for a team of experts with a lot of time and money. A lot of the work in the 21st century has been to scale these theoretical methods to real languages. Most of the really big verification projects of today were unthinkable a decade ago. A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests. Right now the infrarstructure is just not there yet, and that's one of the reasons why formal verification is so expensive. But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...

by fmap 10y ago

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.

fmap 10y ago
> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. You are seriously overselling these results. Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates. > 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 point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction. > Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. You give an example of a termination problem which is equivalent to the consistency of ZFC. Does the consistency of ZFC "elude the power of math"? It's certainly a very simple question, much easier to write down than the Turing machine in question. > Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem. This applies to mathematics as well. You can write down simple sounding questions, like the Collatz conjecture you mention, which are actually extremely complicated. This is the point where complexity theory comes into the picture. For instance, I could generate random types in the calculus of constructions (random propositions) and ask if that type is inhabited (the proposition is provable). This is an undecidable problem and for complexity theoretic reason most instances (of a certain shape) will actually be hard. The concepts in programming aren't inherently more complicated than the concepts in mathematics. If anything, there are plenty of natural concepts in mathematics which behave far more chaotically than anything in CS (look at a table of homotopy groups of spheres and tell me where that pattern comes from). > 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. It's very much the goal for PLT. :) In practice, it's also very much in the future. Right now verifying large programs is possible for a team of experts with a lot of time and money. A lot of the work in the 21st century has been to scale these theoretical methods to real languages. Most of the really big verification projects of today were unthinkable a decade ago. A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests. Right now the infrarstructure is just not there yet, and that's one of the reasons why formal verification is so expensive. But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...