Related to What is the easiest proof assistant to start with? – I suppose familiarity with programming in general would be beneficial to learning how to work with proof assistants. But which kind of programming languages (used in 'regular' programming, think the top 100 tags on Stack Overflow) would be most helpful? Do functional programming languages offer benefits over object-oriented or procedural ones?
$\begingroup$
$\endgroup$
0
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
3
This is a trick question, since proof assistants are also themselves programming languages.
If we had to choose among languages which are not full blown proof assistants, I would choose a pure functional programming language like Haskell.
I think functional programming languages are best for this purpose for two reasons:
- Their rich type systems
- Stateless/equational description of objects
Modern proof assistants usually hinge on the idea of type system. A type is a tag that is associated with data saying that it falls into a certain semantic category. Many programming languages have a type checker that check whether the rules of these types (typing rules) are being respected by the program. In a way, this is like checking whether the programmer is respecting the promises she is making.
However, type systems can be enriched to such an extent that rigorous mathematical propositions can be expressed by them. Most popular proof assistants, including Agda, Coq and Lean are based on expressing mathematical propositions in the form of such typing systems (usually known as a dependent type system).
Haskell has a very rich type system. It is not a full blown dependent type system where arbitrary theorems can be expressed, but it is significantly richer than most other mainstream languages.
Equational reasoning applies easily to functional languages. Since objects in functional languages are referentially transparent and immutable, one can apply lemmas directly to say something about an object without having to worry very much.
There are already attempts to enrich the type system of Haskell so that somewhat simple theorems can be proven. For instance, see the Liquid Haskell homepage.
There are also verification aware languages like Dafny where one can add annotate their programs with theorems. Dafny is not limited to functional programming. It also allows proving imperative programs through techniques like hoare logic and loop invariants. Sadly, Dafny is not a mainstream language
answered Feb 8, 2022 at 20:15
-
$\begingroup$ Haskell is definitely a valid answer, thanks. I've clarified the question to indicate which languages I would consider. $\endgroup$ Commented Feb 8, 2022 at 20:17
-
3$\begingroup$ In addition to enhancements like Liquid Haskell, vanilla (GHC) Haskell and some other languages like OCaml support Generalized Algebraic Data Types (GADTs), which enable a good deal of proof-assistant-like behavior. $\endgroup$ Commented Feb 9, 2022 at 19:38
-
1$\begingroup$ “since proof assistants are also themselves programming languages.” – I’d qualify this with “most”. I am not sure if I’d count the raw Isabelle logic as a programming language. $\endgroup$ Commented Mar 3, 2022 at 21:05
$\begingroup$
$\endgroup$
Proof assistants in declarative programming languages are notable, and a study of Prolog is recommended for context.
Richard O'Keefe said "Prolog is an efficient programming language because it is a very stupid theorem prover." Execution of Prolog programs amounts to SLD resolution for Horn clauses, a decidable fragment of first-order logic.
Herman Geuver's essay "Proof assistants: History, ideas and future" (2009) mentions declarative language in this context about a dozen times. Sec. 1.3 illustrates the input of a Coq formalized proof, first in a procedural style and then in a declarative style. In doing so the paper of Pierre Corbineau, "A Declarative Language For The Coq Proof Assistant" (2007), is cited.
The Mizar system uses a declarative style language (also called Mizar), which Corbineau credits as the "first proof assistant to implement a declarative style proof language".
The declarative approach was carried forward by Isabelle/Isar. Some interest in the status of declarative proof languages in proof assistants can be found at Math.SE from some years back.
$\begingroup$
$\endgroup$
2
An old (vintage / classic) functional language that has been specifically designed for proof assistants is the Standard ML language. Quoting the book ML for the Working Programmer
Every successful language was designed for some specific purpose: Lisp for artificial intelligence, Fortran for numerical computation, ... ML was designed for theorem proving.
The same book even contains a chapter devoted to writing a FOL tactical theorem prover from scratch.
-
$\begingroup$ "Old"? I think you mean vintage or classic ;) $\endgroup$ Commented Feb 10, 2022 at 22:31
-
$\begingroup$ @AlexNelson That's exactly what I mean. $\endgroup$– tinlyxCommented Feb 11, 2022 at 0:31