15 ms·

> Because only a vanishingly rare amount of the incorrectness in compiled C programs comes from a bug in the compiler. True. What I meant to say, but didn't,

by 110011 9y ago

> Because only a vanishingly rare amount of the incorrectness in compiled C programs comes from a bug in the compiler. True. What I meant to say, but didn't, is, why aren't more people working on ensuring that this provability bubbles up from the compiler to the program itself. I come across a lot of work in specialized areas on this topic but haven't seen anyone have a go integrating formal proofs and a widely used programming language. At the moment this looks like a pipe dream because of the obvious objection (and I hope this disappears "soon") that currently it is too cumbersome to have to prove your programs, let alone write them in the first place.

seanmcdirmid 9y ago
The biggest problem in formal program verification is the lack of a spec to verify against for most programs. There are projects like ur web that define correctness more broadly to get around that.
- catnaroek 9y ago
  Ur/Web doesn't redefine “correctness”, since, by definition, your program specification is the definition of what it means for your program to be “correct”. Ur/Web merely guarantees the absence of certain behaviors in programs written in it.
- pron 9y ago
  That's certainly a problem, but it's not the biggest problem. Writing a formal spec is no harder than writing tests (and arguably easier). It doesn't have to be perfect -- the more correctness conditions the better. Of course, a complete spec -- one that says, anything that satisfies this is a correct implementation of the system -- is best, but it's really not required to start getting real benefits. I'd say that the biggest problem is the intractability of verification. Xavier Leroy has said that his style of verification -- end-to-end (i.e., global correctness conditions verified all the way down to source- and machine-code) and employing formal proofs -- is only suitable to the smallest and simplest programs (he claims it's suitable to programs hundreds to thousands of lines long, and even he had to take a few shortcuts in CompCert, e.g., he eschewed some termination proofs). Model-checking fares only a little better, and static analysis -- which scales to arbitrarily-sized programs -- can only verify specific, and mostly local correctness properties. Other approaches can tractably verify global correctness conditions, but only against high-level descriptions of the algorithm/system, and don't reach all the way down to code. AFAIK, the most robust, and still scalable, formal verification employed in real-world programs of considerable size is that employed by Altran UK. They verify global properties against a high-level spec (verified mostly with model-checking, and possibly some proofs), plus local properties at the code level (verified mostly automatically with SMT solvers with a small number of manual proofs), but leaving a gap in between. This could very well become easier and scale well, and could become affordable (as it automates relatively well) yet still extremely useful, as end-to-end verification is hardly ever required. They're using Z for the high-level spec and Ada SPARK for the code-level spec, but other tools could be used (e.g. TLA+/Alloy for the high level, and JML/ACSL/Clojure Spec/Spec# for the code level). I've personally successfully used refinement mappings in TLA+, which allow you to move between different levels of the system description, with the different specs as well as the refinement mapping itself checked with a model checker. This is indeed harder than just checking a single description, but still in the realm of affordability. Taking refinements all the way down to the source level is still far from affordable, though.
  - neel_k 9y ago
    > [...] even he had to take a few shortcuts in CompCert, e.g., he eschewed some termination proofs. This turned out to be a premature optimization, actually! The CakeML compiler did full functional correctness proofs for their register allocator and report that it wasn't significantly harder than Compcert's translation validation. > Writing a formal spec is no harder than writing tests (and arguably easier). This, I'm much less sure of. IME, the really hard thing about correctness proofs is that specifications and proofs often require genuinely new ideas that didn't occur in the code. For example, the spec of something like a sorting routine is that the output returns a list in increasing order, and that the output is a permutation of the input. The concept of a permutation doesn't occur explicitly in the implementation of the sort, and so the need to make this concept explicit can stop learners dead in their tracks. I taught Agda (a dependently-typed programming language) to undergraduates, and found that Agda-the-programming language was actually easier to teach than Haskell (the IDE is better and there's less magic). But Agda-the-proof-assistant was hard to teach, mostly AFAICT because I don't know how to teach having mathematical ideas well.
    - pron 9y ago
      > Agda-the-proof-assistant was hard to teach, mostly AFAICT because I don't know how to teach having mathematical ideas well. One of the (several) problems I find with dependently-typed languages is that they don't easily allow you to separate specification from verification [1]. When using a language like TLA+, it's very easy to separate the two. I actually think it's easier to teach mathematical thinking with TLA+ than without any formal language at all, as you can get feedback as to what has gone wrong, i.e, you can "play" with the math, and use the model checker before writing a proof to get a counterexample. I agree that teaching how to think mathematically is still required and still hard, but there's much less accidental complexity in the way. Another advantage is that complex concepts are only encountered later [2] (e.g., you can cleanly separate safety from the much more complex liveness). The only downside (for teaching) is that the proofs are declarative, so you don't get to teach actual syntactic manipulation of terms (which is, arguably, not important unless you want to teach low-level proofs). Of course, the computational theory is TLA rather than lambda calculus, so it's irrelevant if you want to teach that formal system in particular. On the other hand, advanced and very powerful concepts such as refinement are very elegant and relatively simple. [1]: Another is that proof is pretty much the only form of verification (of specification given as types), which is both extremely costly and very rarely required, and yet another is that complicated matters are encountered very early on. [2] I've been playing with Lean for some weeks, and I still don't understand what object `id` (the identity "function", polymorphic over all types in all universes) is; all I know is that it's not an actual function. I'm not sure whether it's the same or not in Agda.

by 110011 9y ago

seanmcdirmid 9y ago

The biggest problem in formal program verification is the lack of a spec to verify against for most programs. There are projects like ur web that define correctness more broadly to get around that.

catnaroek 9y ago
Ur/Web doesn't redefine “correctness”, since, by definition, your program specification is the definition of what it means for your program to be “correct”. Ur/Web merely guarantees the absence of certain behaviors in programs written in it.
pron 9y ago
That's certainly a problem, but it's not the biggest problem. Writing a formal spec is no harder than writing tests (and arguably easier). It doesn't have to be perfect -- the more correctness conditions the better. Of course, a complete spec -- one that says, anything that satisfies this is a correct implementation of the system -- is best, but it's really not required to start getting real benefits. I'd say that the biggest problem is the intractability of verification. Xavier Leroy has said that his style of verification -- end-to-end (i.e., global correctness conditions verified all the way down to source- and machine-code) and employing formal proofs -- is only suitable to the smallest and simplest programs (he claims it's suitable to programs hundreds to thousands of lines long, and even he had to take a few shortcuts in CompCert, e.g., he eschewed some termination proofs). Model-checking fares only a little better, and static analysis -- which scales to arbitrarily-sized programs -- can only verify specific, and mostly local correctness properties. Other approaches can tractably verify global correctness conditions, but only against high-level descriptions of the algorithm/system, and don't reach all the way down to code. AFAIK, the most robust, and still scalable, formal verification employed in real-world programs of considerable size is that employed by Altran UK. They verify global properties against a high-level spec (verified mostly with model-checking, and possibly some proofs), plus local properties at the code level (verified mostly automatically with SMT solvers with a small number of manual proofs), but leaving a gap in between. This could very well become easier and scale well, and could become affordable (as it automates relatively well) yet still extremely useful, as end-to-end verification is hardly ever required. They're using Z for the high-level spec and Ada SPARK for the code-level spec, but other tools could be used (e.g. TLA+/Alloy for the high level, and JML/ACSL/Clojure Spec/Spec# for the code level). I've personally successfully used refinement mappings in TLA+, which allow you to move between different levels of the system description, with the different specs as well as the refinement mapping itself checked with a model checker. This is indeed harder than just checking a single description, but still in the realm of affordability. Taking refinements all the way down to the source level is still far from affordable, though.
- neel_k 9y ago
  > [...] even he had to take a few shortcuts in CompCert, e.g., he eschewed some termination proofs. This turned out to be a premature optimization, actually! The CakeML compiler did full functional correctness proofs for their register allocator and report that it wasn't significantly harder than Compcert's translation validation. > Writing a formal spec is no harder than writing tests (and arguably easier). This, I'm much less sure of. IME, the really hard thing about correctness proofs is that specifications and proofs often require genuinely new ideas that didn't occur in the code. For example, the spec of something like a sorting routine is that the output returns a list in increasing order, and that the output is a permutation of the input. The concept of a permutation doesn't occur explicitly in the implementation of the sort, and so the need to make this concept explicit can stop learners dead in their tracks. I taught Agda (a dependently-typed programming language) to undergraduates, and found that Agda-the-programming language was actually easier to teach than Haskell (the IDE is better and there's less magic). But Agda-the-proof-assistant was hard to teach, mostly AFAICT because I don't know how to teach having mathematical ideas well.
  - pron 9y ago
    > Agda-the-proof-assistant was hard to teach, mostly AFAICT because I don't know how to teach having mathematical ideas well. One of the (several) problems I find with dependently-typed languages is that they don't easily allow you to separate specification from verification [1]. When using a language like TLA+, it's very easy to separate the two. I actually think it's easier to teach mathematical thinking with TLA+ than without any formal language at all, as you can get feedback as to what has gone wrong, i.e, you can "play" with the math, and use the model checker before writing a proof to get a counterexample. I agree that teaching how to think mathematically is still required and still hard, but there's much less accidental complexity in the way. Another advantage is that complex concepts are only encountered later [2] (e.g., you can cleanly separate safety from the much more complex liveness). The only downside (for teaching) is that the proofs are declarative, so you don't get to teach actual syntactic manipulation of terms (which is, arguably, not important unless you want to teach low-level proofs). Of course, the computational theory is TLA rather than lambda calculus, so it's irrelevant if you want to teach that formal system in particular. On the other hand, advanced and very powerful concepts such as refinement are very elegant and relatively simple. [1]: Another is that proof is pretty much the only form of verification (of specification given as types), which is both extremely costly and very rarely required, and yet another is that complicated matters are encountered very early on. [2] I've been playing with Lean for some weeks, and I still don't understand what object `id` (the identity "function", polymorphic over all types in all universes) is; all I know is that it's not an actual function. I'm not sure whether it's the same or not in Agda.