|
Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware systems. The people using theorem provers are diverse in their tasks and priorities. Consider three provers/languages: Coq, ACL2, and Dafny. Coq is a very expressive, dependently-typed, higher-order functional language, much in the spirit of Haskell or SML. It is very powerful for writing specifications due to this expressivity, and is therefore a compelling candidate for formalizing mathematics. It also has a very clean separation between proof search and proof checking, allowing for a smaller trusted kernel in the proof checker. However, due to the complexity of the language, writing proofs tends to be a largely manual task, or require domain-specific automation. ACL2, on the other hand, is simpler in its language. It is a first order logic, built atop a total, untyped (at least logically) lisp. It does not produce proof artifacts like Coq, but proofs are much more automated, consisting of only a handful of hints instead of an entire tactic-tree. Finally, Dafny is an imperative language, very much resembling popular and ubiquitous languages familiar to every programmer. Proofs are managed by adding inline annotations, specifying pre and postconditions, invariants, etc. This does not expose hardly any of the proof internals, and may be difficult for large proofs, but is a relatively friendly interface for the working software engineer. |