4 ms·

Compared with Coq, F* makes it easier to write programs with side effects, i.e., actually mutate variables and memory. There is a language fragment which amount

Compared with Coq, F* makes it easier to write programs with side effects, i.e., actually mutate variables and memory. There is a language fragment which amounts to programming in a subset of C (and this is used for generating C code for the verified crypto stuff in Project Everest mentioned in other comments). Also compared with Coq, proofs rely heavily on SMT solving with Z3 instead of lots of manual tactics (yay!). On the other hand, where SMT solving fails, you can not resort to manual tactics because there is no tactic language. You have to write proof terms without interactive support. (This may have changed in the last few months, but I'm almost sure it hasn't.) I wrote a bit about my experiences trying to prove things in F* two years ago: https://news.ycombinator.com/item?id=10984306 https://news.ycombinator.com/item?id=10984306 Don't rely on any of that though, things will have changed in the meantime! I'm optimistic about F*, but at the moment you have to be quite determined to try to use it for fully verified programming. The same is true for Coq, though.

gnulinux 9y ago
Which language, do you think, is most practical for writing formally verified programs?
- neel_k 9y ago
  Probably the four most well-known pieces of software with end-to-end verification of functional correctness are the CertiKOS microkernel from Yale (verified in Coq), the SEL4 microkernel (verified in Isabelle), the Compcert C compiler (verified in Coq), the CakeML ML compiler (verified in Isabelle). Stopping short of full end-to-end functional correctness, there are lot more notable examples, such as the Verve system at MSR (verified type/memory safety using Boogie), and the Bedrock system at MIT (functional correctness down to a fairly low-level IR, done in Coq), the miTLS/Everest TLS stack (protocol correctness verified in F-star, most of the way down to a C-like implementation), and the Iris project (a toolkit for verifying higher-order concurrent programs, currently being used to formalize Rust including unsafe, in Coq). In machine-checked proof, the three biggest successes are the verification of the Odd Order Theorem (in Coq), the Four Colour Theorem (in Coq), and the Flyspeck project verifying the proof of the Kepler conjecture (in HOL). In hardware verification, there has been a huge amount of work using ACL2 and HOL, but I don't know this space as well. Basically, Coq and Isabelle have the most actual successes, but other things like F-star, Boogie and HOL have all worked as well.
  - gnulinux 9y ago
    Magnificient answer. Thank you.
  - logicchains 9y ago
    CakeML was verified in HOL (https://hol-theorem-prover.org/ https://hol-theorem-prover.org/), not Isabelle.
    - neel_k 9y ago
      Yes, you're right. Thanks for the correction!
- tom_mellior 9y ago
  In addition to the great sibling comment by neel_k: It depends. I don't think that currently there is the one system that is uniformly best. For example, I wouldn't want to try to write the kind of fiddling with byte arrays involved in cryptography in Coq. F* is certainly better for that. I imagine Dafny is better for it, too. Possibly Why3 as well. Or, if that is really what you want, you might even go for "real" programming languages (ones that exist independently of verification frameworks) such as Ada with SPARK/Ada or C with Frama-C. If you want to verify purely functional programs, Coq is pretty good, but proving is often boringly manual. Also, the language is more influenced by the OCaml branch of the ML family than by Haskell; for Haskellers there are Idris and Agda. Then there is Isabelle/HOL, which has a lot of proof automation but a bizarre logic. Oh, I haven't even mentioned Lean. Well. There is really no easy answer: You have to try to get acquainted with several of the frameworks, ideally with an idea for what your application will be. And whichever you choose, it will be hard.
  - mcguire 9y ago
    Having played with dependently typed languages (ATS, Idris) some, and with verification tools (SPARK/Ada, Frama-C/C), I'd like to go a little farther and say that the verification tools are much more like "normal programming" rather than building a proof with the side effect of creating a program. https://maniagnosis.crsr.net/tags/applied%20formal%20logic.html https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h...
  - cmrx64 9y ago
    In what way is HOL bizarre?
    - tom_mellior 9y ago
      First, just to clarify, I wrote "Isabelle/HOL", and I'm not claiming anything about any of the many many other systems that have "HOL" in their name. I don't know those. That said, I think the thing that annoyed me most were the different language levels: "assume P show Q" and "P ==> Q" are both implications, but somehow different. I never quite understood why and how, but there seem to be cases where only one can be proved but not the other. Similarly for different kinds of universal quantification. Your interpretation of "bizarre" may very well vary, but I found these unintuitive and not explained well in the documentation that I found. (Don't ask for anything much more concrete than this. It's been a while, and I've forgotten the details.)
- nickpsecurity 9y ago
  For small modules, SPARK with this book from the limited feedback I have: https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-... Verification of larger programs is hard for a lot of reasons. Easiest method is to do Design-by-Contract in a memory-safe language. Anything easy to specify in contracts goes there where stuff easier to test for is done that way. If your language doesn't support it, you can do it with asserts, conditionals in functions, or constructors/destructors in OOP. http://www.eiffel.com/developers/design_by_contract_in_detail.html http://www.eiffel.com/developers/design_by_contract_in_detai... Then, you hit the app with tests generated from the contracts and fuzz testing that both run while the contract conditions have runtime checks in the code. That means a failure will take you right to the precondition, invariant, or post condition that is broken. For analyzing distributed stuff, TLA+ is your best bet with an accessible tutorial for a subset available here: https://learntla.com/introduction/ https://learntla.com/introduction/
beurdouche 9y ago
F* now has tactics, it is very new, but no doubt that it will evolve a lot... https://github.com/FStarLang/FStar/tree/master/examples/tactics https://github.com/FStarLang/FStar/tree/master/examples/tact...
- tom_mellior 9y ago
  Cool! Can you develop them interactively in Emacs, like in Coq, observing how individual tactics change the proof state?
  - mtzguido 9y ago
    Sadly not yet. You can see each individual intermediate state but the thing runs fully. We certainly plan to add such a feature though! We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).

gnulinux 9y ago

Which language, do you think, is most practical for writing formally verified programs?

neel_k 9y ago
Probably the four most well-known pieces of software with end-to-end verification of functional correctness are the CertiKOS microkernel from Yale (verified in Coq), the SEL4 microkernel (verified in Isabelle), the Compcert C compiler (verified in Coq), the CakeML ML compiler (verified in Isabelle). Stopping short of full end-to-end functional correctness, there are lot more notable examples, such as the Verve system at MSR (verified type/memory safety using Boogie), and the Bedrock system at MIT (functional correctness down to a fairly low-level IR, done in Coq), the miTLS/Everest TLS stack (protocol correctness verified in F-star, most of the way down to a C-like implementation), and the Iris project (a toolkit for verifying higher-order concurrent programs, currently being used to formalize Rust including unsafe, in Coq). In machine-checked proof, the three biggest successes are the verification of the Odd Order Theorem (in Coq), the Four Colour Theorem (in Coq), and the Flyspeck project verifying the proof of the Kepler conjecture (in HOL). In hardware verification, there has been a huge amount of work using ACL2 and HOL, but I don't know this space as well. Basically, Coq and Isabelle have the most actual successes, but other things like F-star, Boogie and HOL have all worked as well.
- gnulinux 9y ago
  Magnificient answer. Thank you.
- logicchains 9y ago
  CakeML was verified in HOL (https://hol-theorem-prover.org/ https://hol-theorem-prover.org/), not Isabelle.
  - neel_k 9y ago
    Yes, you're right. Thanks for the correction!
tom_mellior 9y ago
In addition to the great sibling comment by neel_k: It depends. I don't think that currently there is the one system that is uniformly best. For example, I wouldn't want to try to write the kind of fiddling with byte arrays involved in cryptography in Coq. F* is certainly better for that. I imagine Dafny is better for it, too. Possibly Why3 as well. Or, if that is really what you want, you might even go for "real" programming languages (ones that exist independently of verification frameworks) such as Ada with SPARK/Ada or C with Frama-C. If you want to verify purely functional programs, Coq is pretty good, but proving is often boringly manual. Also, the language is more influenced by the OCaml branch of the ML family than by Haskell; for Haskellers there are Idris and Agda. Then there is Isabelle/HOL, which has a lot of proof automation but a bizarre logic. Oh, I haven't even mentioned Lean. Well. There is really no easy answer: You have to try to get acquainted with several of the frameworks, ideally with an idea for what your application will be. And whichever you choose, it will be hard.
- mcguire 9y ago
  Having played with dependently typed languages (ATS, Idris) some, and with verification tools (SPARK/Ada, Frama-C/C), I'd like to go a little farther and say that the verification tools are much more like "normal programming" rather than building a proof with the side effect of creating a program. https://maniagnosis.crsr.net/tags/applied%20formal%20logic.html https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h...
- cmrx64 9y ago
  In what way is HOL bizarre?
  - tom_mellior 9y ago
    First, just to clarify, I wrote "Isabelle/HOL", and I'm not claiming anything about any of the many many other systems that have "HOL" in their name. I don't know those. That said, I think the thing that annoyed me most were the different language levels: "assume P show Q" and "P ==> Q" are both implications, but somehow different. I never quite understood why and how, but there seem to be cases where only one can be proved but not the other. Similarly for different kinds of universal quantification. Your interpretation of "bizarre" may very well vary, but I found these unintuitive and not explained well in the documentation that I found. (Don't ask for anything much more concrete than this. It's been a while, and I've forgotten the details.)
nickpsecurity 9y ago
For small modules, SPARK with this book from the limited feedback I have: https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-... Verification of larger programs is hard for a lot of reasons. Easiest method is to do Design-by-Contract in a memory-safe language. Anything easy to specify in contracts goes there where stuff easier to test for is done that way. If your language doesn't support it, you can do it with asserts, conditionals in functions, or constructors/destructors in OOP. http://www.eiffel.com/developers/design_by_contract_in_detail.html http://www.eiffel.com/developers/design_by_contract_in_detai... Then, you hit the app with tests generated from the contracts and fuzz testing that both run while the contract conditions have runtime checks in the code. That means a failure will take you right to the precondition, invariant, or post condition that is broken. For analyzing distributed stuff, TLA+ is your best bet with an accessible tutorial for a subset available here: https://learntla.com/introduction/ https://learntla.com/introduction/

beurdouche 9y ago

F* now has tactics, it is very new, but no doubt that it will evolve a lot... https://github.com/FStarLang/FStar/tree/master/examples/tactics https://github.com/FStarLang/FStar/tree/master/examples/tact...

tom_mellior 9y ago
Cool! Can you develop them interactively in Emacs, like in Coq, observing how individual tactics change the proof state?
- mtzguido 9y ago
  Sadly not yet. You can see each individual intermediate state but the thing runs fully. We certainly plan to add such a feature though! We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).