3 ms·

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 wou

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.)
  - cmrx64 9y ago
    Fair enough :) FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and the automation tends to normalize object-level quantification and implication into meta-level. "assume P show Q" is just Isar-syntax for a structured proof of "P ==> Q" (which is a term).

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.)
- cmrx64 9y ago
  Fair enough :) FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and the automation tends to normalize object-level quantification and implication into meta-level. "assume P show Q" is just Isar-syntax for a structured proof of "P ==> Q" (which is a term).