6 ms·

> [...] 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! T

by 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.
- xgk 9y ago
  > to separate specification from verification Exactly. Program logics are superior in this regard: the encourage rather than inhibit separation of concerns. (Not to mention: program logics are more developed and cover a large class of computing paradigms, while dependent types have not grown much beyond the pure functions ghetto.) I put forward this point to dependent types luminaries all the time. Its difficult to get more than polite silence in response. * * * It's partly a social problem: The community working on dependently typed languages and tools typically have most of their programming experience with pure functional languages. Exaggerating only a bit, here is the typical trajectory of a formal methods researcher: - As an undergraduate writes a lambda-calculus interpreter in Lisp/Scheme/Racket/Haskell - As a PhD Student writes their own pure language with wacky typing system, and demonstrate its usefulness by embedding a lambda-calculus interpreter in it. - As a postdoc verifies a lambda-calculus interpreter in Coq/Agda. - As an assistant professor writes their own Curry-Howard-based interactive prover in some dependently typed language and demonstrate its usefulness by verifying a lambda-calculus interpreter in it. - After tenure, gets their students to do the above. 2018's POPL has a type-theory in type-theory paper, but none on how programming language theory can improve SAT solving ... It's an echo chamber. I recently reviewed a grant proposal by some of the more famous dependent types researchers. They proposed using HoTT to verify computational effects. The grant proposal claimed (1) that there is currently no known way to verify effectful languages and (2) that embedding generalisations of effect monads in HoTT is the way to overcome this problem. It seems like these people have not ever heard of program logics? * * * A second reason is more serious: the real problem of formal verification is not this-language/that-logic. In day-to-day verification, it doesn't really matter that much whether you are using this/that approach. You need to set up the right definitions and invariants. That's the hard part. Whether you express them in some program logic or dependently typed system doesn't matter much, you can usually transliterate between them. The real problem is automation. Better autmation means dramatically better SAT solvers (modern SMT solvers are heavily reliant of SAT solvers). It's just unclear where 10x, 100x, 1000x speedups in SAT solvers should come from. We don't even know how to parallelise SAT solvers well. In the absence of dramatic progress in SAT solvers, what can we do other than tinkering with dependently typed languages and their relatives?
catnaroek 9y ago
Clearly, the only way forward is to make programming attractive to mathematicians, since making mathematics attractive to programmers has largely failed.
- pron 9y ago
  I'm not at all sure mathematicians would make better programmers. One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their is a corresponding equivalence of the two activities. This is somewhat analogous to concluding that since both programming and writing involve entering words into a text editor, the two are the same. But the fact that, from some specific perspective, both mathematicians and programmers write proofs does not mean that the activities are similar. Both physicists and mathematicians solve equations, but no one would say that physics is math. Mathematicians manipulate objects that are very different from those that programmers manipulate. Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable, while programmers manipulate very irregular and very intractable objects. Ostensibly, the difference is only in measure, but a difference in any robust complexity measure is usually a difference in quality. Even the actual proofs are very different. Mathematical proofs are usually short but mathematically deep, while program proofs are mathematically shallow and uninteresting, but very, very long and full of detail. Not to mention that the motivations are completely different. The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable), and increasing the cost of programming by an order of magnitude in order to make all bugs provably absent is the wrong thing to do. In math, the requirements are completely different.
  - catnaroek 9y ago
    > One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their[sic] is a corresponding equivalence of the two activities. Don't take this as an endorsement of proof assistants, but programming and proving are special cases of a single general activity: constructing a mathematical object. > Both physicists and mathematicians solve equations, but no one would say that physics is math. The crucial difference is that physicists, unlike mathematicians or programmers, don't create universes of their own. Their job is to explain the behavior of the one that already exists. > Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable Only because they have made them so. Also, insanely irregular and intractable mathematical objects do exist, yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof. > while programmers manipulate very irregular and very intractable objects. Only because they have made them so. Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning. > The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity Then quantify the bug, and make it a part of the specification. > (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable) Bugs occur in the program, not in its execution traces.
tom_mellior 9y ago
> 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. Not sure if you're saying that using a translation validation approach for register allocation was a premature optimization. But if that's what you're saying, you're wrong: The paper describing the register allocation validator explains that this replaced a register allocator in Coq that was proved directly. The validator approach is much smaller and simpler than this direct proof was. So it was an actual optimization after the fact. It's possible that CakeML does it better, of course.
- neel_k 9y ago
  That's interesting! I heard this from some CakeML people, who told me they decided to go with a full proof because it wasn't much more work for them. Maybe Compcert has a fancier register allocator architecture that benefits more from translation validation?
  - tom_mellior 9y ago
    Maybe, but on the other hand maybe the CakeML developers have some proof techniques that the CompCert people didn't think of. I don't know. For reference, my only knowledge of this point comes from the CC 2010 paper at https://xavierleroy.org/publi/validation-regalloc.pdf https://xavierleroy.org/publi/validation-regalloc.pdf, which says in section 5: "From a proof engineering viewpoint, the validator is a success. Its mechanized proof of correctness is only 900 lines of Coq, which is quite small for a 350-line piece of code. (The typical ratio for Coq program proofs is 6 to 8 lines of proof per line of code.) In contrast, 4300 lines of Coq proof were needed to verify the register allocation and spilling passes of the original CompCert compiler. Even this earlier development used translation validation on a sub-problem: the George-Appel graph coloring algorithm was implemented directly in untrusted Caml code, then followed by a verified validator to check that the resulting as- signment is a valid coloring of the interference graph. Later, Blazy, Robillard and Appel conducted a Coq proof of the graph coloring algorithm [13]. This is a fairly large proof: in total, more than 10000 lines of proof are needed to com- pletely verify the original CompCert register allocation and spilling passes." (And hence my statement above was also inaccurate in that the original CompCert was not fully directly proven. I had misremembered the details of this paragraph. The point still stands that the newer validation solution is simpler.)

by neel_k 9y ago

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.

xgk 9y ago
> to separate specification from verification Exactly. Program logics are superior in this regard: the encourage rather than inhibit separation of concerns. (Not to mention: program logics are more developed and cover a large class of computing paradigms, while dependent types have not grown much beyond the pure functions ghetto.) I put forward this point to dependent types luminaries all the time. Its difficult to get more than polite silence in response. * * * It's partly a social problem: The community working on dependently typed languages and tools typically have most of their programming experience with pure functional languages. Exaggerating only a bit, here is the typical trajectory of a formal methods researcher: - As an undergraduate writes a lambda-calculus interpreter in Lisp/Scheme/Racket/Haskell - As a PhD Student writes their own pure language with wacky typing system, and demonstrate its usefulness by embedding a lambda-calculus interpreter in it. - As a postdoc verifies a lambda-calculus interpreter in Coq/Agda. - As an assistant professor writes their own Curry-Howard-based interactive prover in some dependently typed language and demonstrate its usefulness by verifying a lambda-calculus interpreter in it. - After tenure, gets their students to do the above. 2018's POPL has a type-theory in type-theory paper, but none on how programming language theory can improve SAT solving ... It's an echo chamber. I recently reviewed a grant proposal by some of the more famous dependent types researchers. They proposed using HoTT to verify computational effects. The grant proposal claimed (1) that there is currently no known way to verify effectful languages and (2) that embedding generalisations of effect monads in HoTT is the way to overcome this problem. It seems like these people have not ever heard of program logics? * * * A second reason is more serious: the real problem of formal verification is not this-language/that-logic. In day-to-day verification, it doesn't really matter that much whether you are using this/that approach. You need to set up the right definitions and invariants. That's the hard part. Whether you express them in some program logic or dependently typed system doesn't matter much, you can usually transliterate between them. The real problem is automation. Better autmation means dramatically better SAT solvers (modern SMT solvers are heavily reliant of SAT solvers). It's just unclear where 10x, 100x, 1000x speedups in SAT solvers should come from. We don't even know how to parallelise SAT solvers well. In the absence of dramatic progress in SAT solvers, what can we do other than tinkering with dependently typed languages and their relatives?

catnaroek 9y ago

Clearly, the only way forward is to make programming attractive to mathematicians, since making mathematics attractive to programmers has largely failed.

pron 9y ago
I'm not at all sure mathematicians would make better programmers. One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their is a corresponding equivalence of the two activities. This is somewhat analogous to concluding that since both programming and writing involve entering words into a text editor, the two are the same. But the fact that, from some specific perspective, both mathematicians and programmers write proofs does not mean that the activities are similar. Both physicists and mathematicians solve equations, but no one would say that physics is math. Mathematicians manipulate objects that are very different from those that programmers manipulate. Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable, while programmers manipulate very irregular and very intractable objects. Ostensibly, the difference is only in measure, but a difference in any robust complexity measure is usually a difference in quality. Even the actual proofs are very different. Mathematical proofs are usually short but mathematically deep, while program proofs are mathematically shallow and uninteresting, but very, very long and full of detail. Not to mention that the motivations are completely different. The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable), and increasing the cost of programming by an order of magnitude in order to make all bugs provably absent is the wrong thing to do. In math, the requirements are completely different.
- catnaroek 9y ago
  > One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their[sic] is a corresponding equivalence of the two activities. Don't take this as an endorsement of proof assistants, but programming and proving are special cases of a single general activity: constructing a mathematical object. > Both physicists and mathematicians solve equations, but no one would say that physics is math. The crucial difference is that physicists, unlike mathematicians or programmers, don't create universes of their own. Their job is to explain the behavior of the one that already exists. > Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable Only because they have made them so. Also, insanely irregular and intractable mathematical objects do exist, yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof. > while programmers manipulate very irregular and very intractable objects. Only because they have made them so. Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning. > The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity Then quantify the bug, and make it a part of the specification. > (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable) Bugs occur in the program, not in its execution traces.

tom_mellior 9y ago

> 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. Not sure if you're saying that using a translation validation approach for register allocation was a premature optimization. But if that's what you're saying, you're wrong: The paper describing the register allocation validator explains that this replaced a register allocator in Coq that was proved directly. The validator approach is much smaller and simpler than this direct proof was. So it was an actual optimization after the fact. It's possible that CakeML does it better, of course.

neel_k 9y ago
That's interesting! I heard this from some CakeML people, who told me they decided to go with a full proof because it wasn't much more work for them. Maybe Compcert has a fancier register allocator architecture that benefits more from translation validation?
- tom_mellior 9y ago
  Maybe, but on the other hand maybe the CakeML developers have some proof techniques that the CompCert people didn't think of. I don't know. For reference, my only knowledge of this point comes from the CC 2010 paper at https://xavierleroy.org/publi/validation-regalloc.pdf https://xavierleroy.org/publi/validation-regalloc.pdf, which says in section 5: "From a proof engineering viewpoint, the validator is a success. Its mechanized proof of correctness is only 900 lines of Coq, which is quite small for a 350-line piece of code. (The typical ratio for Coq program proofs is 6 to 8 lines of proof per line of code.) In contrast, 4300 lines of Coq proof were needed to verify the register allocation and spilling passes of the original CompCert compiler. Even this earlier development used translation validation on a sub-problem: the George-Appel graph coloring algorithm was implemented directly in untrusted Caml code, then followed by a verified validator to check that the resulting as- signment is a valid coloring of the interference graph. Later, Blazy, Robillard and Appel conducted a Coq proof of the graph coloring algorithm [13]. This is a fairly large proof: in total, more than 10000 lines of proof are needed to com- pletely verify the original CompCert register allocation and spilling passes." (And hence my statement above was also inaccurate in that the original CompCert was not fully directly proven. I had misremembered the details of this paragraph. The point still stands that the newer validation solution is simpler.)