There seems to be a robust enough landscape for formal verification that there are definitely some considerations to be made before starting. What should be considered before undertaking a new verification project?
I’ve seen there are a few routes to go for mechanical assistance, i.e. Isabelle, Coq, DAFNY… Does the fact that DAFNY incorporates verification into the semantics of the language strengthen or weaken it? Since Coq can be made to use classical logic, is there an advantage to either Isabelle or Coq.
Any other broad choices to make about application design that are not obvious from the outset?
If you can afford to, the main thing I would recommend is getting at least one person who has experience in verification into the team. Then pick whichever tool that person knows well – there are differences between the tools that matter, but experience in one tool matters much more.
If you are starting and learning from scratch, I’d say Dafny is the easiest to learn and the easiest to be productive with in the beginning, but it forces you to use a specific programming language and verification paradigm.
Spark/Ada if you’re into Ada is similar in that sense, but a bit older.
Coq and Isabelle can in theory support any language and verification method, but in practice unless you want to develop your own framework, there is mostly C and some smaller developments for other languages.
Coq and Isabelle are roughly equal in popularity overall, in the US probably Coq a bit more. In terms of expressive power for program verification, they are both the same. Coq has dependent types, Isabelle has better automation. If you are doing deep mathematics, Coq has the more expressive logic for that. In theory that matters, in practice not so much. If you take lists like this one you might even conclude the opposite. Both provers are successful in math and computer science applications.
I know of big companies successfully using Isabelle and Dafny for program verification, I don’t know any for Coq (I do know some that tried), but that is likely because I follow Isabelle more closely, they are probably out there.
Hey @gerwin.klein, thanks for the response! Very well balanced and insightful. That provides a great start.