This is a comparison of various tools for “verifying” that a piece of code (written in a functional programming style) fulfils a specification, with some degree of automation, to various degrees of confidence.
I’m not putting this on Wikipedia, because many Wikipedia editors will summarily delete supposedly “non-notable” table rows in tables, despite there being no Wikipedia policy to do so.
Note: DSolve is currently not included because the published version does not support recursive types, such as List.
|Name||Available for download||Mode(s)||Solvers||Operates on|
|ScalaCheck3||Yes||Stochastic||None – direct execution||Scala / Any|
1 Dafny really shows that the lines between interactive and automated provers have blurred. It has an intriguing feature – the ability to prove lemmas by giving the solver enough hints to let it prove it by itself, and then have those lemmas be automatically employed by the solver. I am not sure whether any other system offers such a feature, as such.2
2 Coq does not yet integrate with any solvers (other than its built-in decision procedures), though a project is underway to change this. So why would you want to use Coq instead of Isabelle at the present time? Well, one possible reason is that Coq supports dependent types (although not in such a convenient way as languages specifically designed for dependently-typed programming), whereas Isabelle doesn’t.
3 ScalaCheck is one of a family of independently-developed tools named something-Check, which began with QuickCheck (which is for Haskell).
4 These tools (Coq and Isabelle) both support code extraction to proper programming languages. Alternatively, there are front-ends to both which can read e.g. Java code and specifications, and create corresponding proof obligations. So don’t worry about being able to execute your code with reasonable performance outside of the tool – you will be able to.
|Name||Static typing||Proof by induction||Verifying higher-order functions||Natively supports imperative code||IDE|
|Isabelle||Yes||Yes||Yes||No||Emacs or JEdit|
|Coq||Yes||Yes||Yes||No1||Emacs or CoqIDE|
|ACL2||No||Yes||No||No||Emacs or Eclipse|
1 Coq does not support imperative programming “natively”, but it can be done in Coq, using e.g. Ynot or Bedrock.
Corrections and additions can be supplied by comment below or by email; please supply a citation to a reliable source in every case.