5 ms·

How does this compare with other verification tools such as TLA+ or Coq?

by fsloth 9y ago

ahelwer 9y ago
TLA+ is a specification language, not a verification language. There is currently no way of establishing correspondence between a TLA+ spec and the code you (presumably) write to implement that spec. There are benefits to this, like using TLA+ to spec the difficult parts of your system without having to buy the whole formal verification farm.
- pron 9y ago
  Not just that. F* is convenient for code-level specification, much like Ada SPARK, JML/OpenJML for Java, and ACSL/Frama-C for C, but it's quite hard to specify global correctness conditions in it, like "the database is always consistent", or "no data is ever lost", which is where TLA+ shines. The gap between local, code-level correctness properties and global ones is a hard one to cross. I am not aware of any tool that can do both (i.e. end-to-end verification) in a way that isn't excruciatingly hard.
  - hwayne 9y ago
    And not just _that_, but TLA+ is really good at expressing liveness conditions, like "the database is EVENTUALLY consistent" or "the algorithm will eventually terminate." Most other formal methods don't cover that.
    - pron 9y ago
      Right; not out of the box, anyway (many proof assistants are powerful enough for deep embedding of arbitrary logics, but, of course, using them is beyond the affordable reach of nearly all software shops). Many can express termination out of the box, which, in theory, can suffice to express most (all?) liveness properties, certainly many useful ones, but again, this is expressed at the function level, and hard to do for global liveness properties.
Jaxan 9y ago
One difference with Coq is that in Coq everything is constructive. A proof of a precondition is an object and has to be constructed in F* you could use classical logic, things are proven by a solver. (I might be wrong.)
- johncolanduoni 9y ago
  You can add the law of excluded middle in Coq like you can in F*, but it would put you at odds with almost all Coq code.
johncolanduoni 9y ago
F* is more geared towards writing verified but otherwise general purpose code directly. Coq is first and foremost a proof assistant, though there are a number of tools that can help you wed it to other programming languages.
tom_mellior 9y ago
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.

How does this compare with other verification tools such as TLA+ or Coq?

by fsloth 9y ago

How does this compare with other verification tools such as TLA+ or Coq?

TLA+ is a specification language, not a verification language. There is currently no way of establishing correspondence between a TLA+ spec and the code you (presumably) write to implement that spec. There are benefits to this, like using TLA+ to spec the difficult parts of your system without having to buy the whole formal verification farm.

pron 9y ago
Not just that. F* is convenient for code-level specification, much like Ada SPARK, JML/OpenJML for Java, and ACSL/Frama-C for C, but it's quite hard to specify global correctness conditions in it, like "the database is always consistent", or "no data is ever lost", which is where TLA+ shines. The gap between local, code-level correctness properties and global ones is a hard one to cross. I am not aware of any tool that can do both (i.e. end-to-end verification) in a way that isn't excruciatingly hard.
- hwayne 9y ago
  And not just _that_, but TLA+ is really good at expressing liveness conditions, like "the database is EVENTUALLY consistent" or "the algorithm will eventually terminate." Most other formal methods don't cover that.
  - pron 9y ago
    Right; not out of the box, anyway (many proof assistants are powerful enough for deep embedding of arbitrary logics, but, of course, using them is beyond the affordable reach of nearly all software shops). Many can express termination out of the box, which, in theory, can suffice to express most (all?) liveness properties, certainly many useful ones, but again, this is expressed at the function level, and hard to do for global liveness properties.

Jaxan 9y ago

One difference with Coq is that in Coq everything is constructive. A proof of a precondition is an object and has to be constructed in F* you could use classical logic, things are proven by a solver. (I might be wrong.)

johncolanduoni 9y ago
You can add the law of excluded middle in Coq like you can in F*, but it would put you at odds with almost all Coq code.

johncolanduoni 9y ago

F* is more geared towards writing verified but otherwise general purpose code directly. Coq is first and foremost a proof assistant, though there are a number of tools that can help you wed it to other programming languages.

tom_mellior 9y ago

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.