4 ms·

> TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. So, which is it? (0) After you verify a TLA+ specification, you sti

> TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. So, which is it? (0) After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program? (1) The program can be generated from the specification. In this case, the TLA+ specification is a program, although it's written in an unusually high-level language. > Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.

pron 10y ago
> After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program? Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects. > The program can be generated from the specification. Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language. > It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification. Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...
- catnaroek 10y ago
  > 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

> After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program? Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects. > The program can be generated from the specification. Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language. > It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification. Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

catnaroek 10y ago
> 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?