3 ms·

> Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". And we probably never will. AFAICT, our on

> Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". And we probably never will. AFAICT, our only hope is to build large software out of small components that can only be composed in obviously correct ways, so that the bulk of the verification effort is spent on each individual component, rather than on their interactions (a hopeless task). This is reflected in my ML programming style: A function exported by a module must not impose any preconditions on its argument that can't be enforced by the module itself. On the other hand, at a higher-level, a functor (parameterized module) may impose nontrivial preconditions on its argument. > Lamport believes that it may be possible (for a properly amenable spec) using machine learning. That is extremely unpalatable to me. I'm more than perfectly willing to use a different formalism (like TLA+, although I'd like better integration with actual programming languages), but not to resort to massive trial and error (which is what machine learning ultimately boils down to) to generate programs. --- Anyway. What I can take from this whole discussion is: (0) As your original blog post says, there are two ways to look at computation. One view simply pays attention to the physically realizable aspects of computation: nature certainly doesn't care that I want to use bits (or more generally, symbols from a finite alphabet) to represent values from a problem domain, or that this bit means one thing but that bit means another thing. The other view pays attention to how computation can be structured and given useful meanings: the (non-C) programmer in general doesn't care that the same bit pattern can be used to represent different values of different types. (1) If I may use a physical analogy, writing purely functional programs and using equational reasoning on program terms as the basis for verification are akin to trying to solve every physics problem by appeal to conservation laws. The two main drawbacks of this approach are that not every physical system is conservative (we want effects, for which monads provide a solution) and that it's useless for reasoning about time (for which there is no solution). (2) On the other hand, the verification style you advocate, by looking directly at state transitions, is akin to solving physics problems by appealing to the laws of motion, suitably expressed as differential equations. The two main drawbacks of this approach is that it may require lengthier computations (which is less of a problem if the computations can be delegated to a computer) and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others (for which AFAICT there is no solution). (3) Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles?

pron 10y ago
> AFAICT, our only hope is to build large software out of small components that can only be composed in obviously correct ways, so that the bulk of the verification effort is spent on each individual component, rather than on their interactions (a hopeless task). But Schnoebelen's theorem proves this is impossible. (in my post: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...) The post also has an example of that: the foo/bar program, AKA Goldbach's program. bar is correct (i.e., it correctly decides whether its parameter is a prime -- maybe there's a bug in my implementation, but we can assume it's correct). This leaves foo. The first two lines are trivial. This leaves the next three lines (I guess that in Haskell it would be one line). I don't see how you can get more modular and composable than that! And yet, we haven't been able to prove the behavior of those three lines for 300 years, even though they're nothing but a simple decrementing for-loop, a single subtraction operation and a single disjunction! Why? Because bar (i.e. `prime?`), in spite of being correct, has a very complex behavior; it can be reasoned in some contexts, but not in this one. In any event, every attempted project decomposed the problem as much as possible. The task still proved prohibitively expensive (although maybe not for high-assurance development!). > The other view pays attention to how computation can be structured and given useful meanings Almost, but not exactly. The values in machines matter greatly to the machine. The language models are human centric, i.e., they compute with values that matter to humans. But the important point of the post is that the two views are incomparable, as the second requires significantly higher work, i.e., expressing a computation in a way that's meaningful to humans is in itself a significant computational effort. >and that it's useless for reasoning about time (for which there is no solution). And that it doesn't work on real world systems. You can reason equationally about the gravity equation all you like, and compose as many instances as you like. But that wouldn't help you to decide interesting properties. > On the other hand, the verification style you advocate, by looking directly at state transitions I don't have an aesthetic reason to advocate this style. I'm a pragmatist, so I chose it and advocate it because it is the only style that has so far proven to work. That you can pick it up in a week or two instead of six months, and that it supports automated tools that make verification affordable are also great pragmatic advantages. If you show me another one that works as well on real-world systems, I'll be happy to use it. > and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others I'm not sure how you get that. TLA+ handles composition very nicely. There are operators that specifically hide variables, called temporal existential quantification. The formula basically says, "there exists a behavior over these (hidden) state variables, such that those other (observable) variables satisfy X". > Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles? That's above my pay-grade, but TLA can be embedded in FP (in fact, the standard Isabelle distribution contains an embedding of TLA+, as TLA+ uses Isabelle as a backend prover, and I think there are embedings in Coq, too[1]), and FP can be embedded in TLA by conisdering extensional equality only. It's mostly a matter of convenience, possibly for different classes of problems. The thing is that deductive proofs of any kind so far seem untenable in all but extreme circumstances. The problem with approaches that rely on types (and this may be orthogonal to FP, maybe not) to prove interesting logical properties are more rigid, and less able to accommodate more partial forms of verification. Maybe there's work on that, though. As a result of that, the TLA approach (in a general sense) is simply more battle tested, and with better real-world results. [1]: http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf

pron 10y ago

> AFAICT, our only hope is to build large software out of small components that can only be composed in obviously correct ways, so that the bulk of the verification effort is spent on each individual component, rather than on their interactions (a hopeless task). But Schnoebelen's theorem proves this is impossible. (in my post: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...) The post also has an example of that: the foo/bar program, AKA Goldbach's program. bar is correct (i.e., it correctly decides whether its parameter is a prime -- maybe there's a bug in my implementation, but we can assume it's correct). This leaves foo. The first two lines are trivial. This leaves the next three lines (I guess that in Haskell it would be one line). I don't see how you can get more modular and composable than that! And yet, we haven't been able to prove the behavior of those three lines for 300 years, even though they're nothing but a simple decrementing for-loop, a single subtraction operation and a single disjunction! Why? Because bar (i.e. `prime?`), in spite of being correct, has a very complex behavior; it can be reasoned in some contexts, but not in this one. In any event, every attempted project decomposed the problem as much as possible. The task still proved prohibitively expensive (although maybe not for high-assurance development!). > The other view pays attention to how computation can be structured and given useful meanings Almost, but not exactly. The values in machines matter greatly to the machine. The language models are human centric, i.e., they compute with values that matter to humans. But the important point of the post is that the two views are incomparable, as the second requires significantly higher work, i.e., expressing a computation in a way that's meaningful to humans is in itself a significant computational effort. >and that it's useless for reasoning about time (for which there is no solution). And that it doesn't work on real world systems. You can reason equationally about the gravity equation all you like, and compose as many instances as you like. But that wouldn't help you to decide interesting properties. > On the other hand, the verification style you advocate, by looking directly at state transitions I don't have an aesthetic reason to advocate this style. I'm a pragmatist, so I chose it and advocate it because it is the only style that has so far proven to work. That you can pick it up in a week or two instead of six months, and that it supports automated tools that make verification affordable are also great pragmatic advantages. If you show me another one that works as well on real-world systems, I'll be happy to use it. > and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others I'm not sure how you get that. TLA+ handles composition very nicely. There are operators that specifically hide variables, called temporal existential quantification. The formula basically says, "there exists a behavior over these (hidden) state variables, such that those other (observable) variables satisfy X". > Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles? That's above my pay-grade, but TLA can be embedded in FP (in fact, the standard Isabelle distribution contains an embedding of TLA+, as TLA+ uses Isabelle as a backend prover, and I think there are embedings in Coq, too[1]), and FP can be embedded in TLA by conisdering extensional equality only. It's mostly a matter of convenience, possibly for different classes of problems. The thing is that deductive proofs of any kind so far seem untenable in all but extreme circumstances. The problem with approaches that rely on types (and this may be orthogonal to FP, maybe not) to prove interesting logical properties are more rigid, and less able to accommodate more partial forms of verification. Maybe there's work on that, though. As a result of that, the TLA approach (in a general sense) is simply more battle tested, and with better real-world results. [1]: http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf