9
$\begingroup$

In doing research for my next question was going to reference another post in CS Stack Exchange. After reading the answers decided they did not go into enough detail, they leave one with more questions than they answer, or at least I was expecting more in the answers, the question had more detail.

Now that there is a site for Proof Assistants a better answer is needed.


Obviously it should do proofs, obviously it should assist the user in completing the proof or doing the proof if possible (I am not opposed to things like SledgeHammer), obviously it should give the proof not just say it can be proven.

What makes a proof assistant a proof assistant?
What is it deep down that separates it from a common programming language?

Feel free to deviate from this line of thought if it hinders an answer.


EDIT

These edits are to address items raised in comments. I may condense these back into the original part as needed.

A main focus of this question arises from the fact that I am working toward implementing a dependent type proof system. (related question) It will not be interactive and is not a proof of concept because it is just recreating the work of existing type systems but instead of using an ML or dialect of programming language the work will be in Prolog.

$\endgroup$
10
  • 2
    $\begingroup$ This question seems a bit too broad, or too meta. Anyway, I'm not voting down/to close, let the thriving beta community decide. $\endgroup$ Feb 10, 2022 at 13:13
  • $\begingroup$ Re 2): It would be nice (and make the question more focused) to incorporate this into it; meaning, that you are thinking about implementations. Re 3): I agree it would not be closed there, but perhaps you also agree that the Zulip chat follows a quite different, conversational/ephemeral style than SE sites. Re 4): I do not mean as in "meta site", and for the second question, perhaps my comment regarding 2 might explain my intentions. $\endgroup$ Feb 10, 2022 at 13:41
  • $\begingroup$ I saw your edit, +1. $\endgroup$ Feb 10, 2022 at 14:03
  • 4
    $\begingroup$ What I'd really like to know is how to convince @GuyCoder to use emphasize phrases this way and not that way. $\endgroup$ Feb 10, 2022 at 14:42
  • $\begingroup$ OTH, I can see from a mile away that it's your text... $\endgroup$ Feb 10, 2022 at 14:48

2 Answers 2

4
$\begingroup$

Since this question made it back up to the top, let me take a stab. In short, there is going to be no air-tight definition of a "proof assistant" just like there is no air-tight definition of a "programming language". Sure C and Python are probably square in the programming language camp, but what about Brain F***, LaTeX, HTML, SQL, YAML, and some arbitrary macro language? What makes one a programming language and not the other?

The main thing I would say that makes a proof assistant (PA) a proof assistant is intent. That is a PA is indented as a way to assist the user in writing proofs. PAs are also called Interactive Theorem Provers (ITPs), with the same idea: An ITP is intended to be used as an interactive tool for proving theorems (as opposed to an Automated Theorem Prover).

The main area of interactive assistance that a PA/ITP provides is checking the details of a proof. For some proof assistants this checking is (mostly) air-tight logic. (For other, more experimental, proof assistants the user has to be more careful to avoid known inconstancies or unsoundness, but the intent is the same. If you use it as intended it will help you make sure you are following the rules of your proof system. This is even more important with experimental logics since one hasn't built up a good intuition yet of what is and isn't ok.)

Of course, in theory (and maybe even in practice already) it is possible to blend PAs with related tools like markup/document languages, specification languages, programming languages, automated theorem provers, computer algebra systems, and computer games. So it is really a continuum. But let's look at each of these technologies and see how they differ from PAs even if it possible to combine both intents into one tool.

Markup/Document languages

Proof assistants are intended to build and record proofs. The the proofs (and even moreso the theorem statements) need to be written and stored in a human readable way so that (1) the user can enter the proof and (2) the user can find theorems to use for later proofs. (By "human readable", I mean at least as human readable as a computer programming language.) So in that way proof assistants are starting to resemble other tools for writing mathematics, like LaTeX and MathML. But the intent of proof assistants is different. LaTeX's and MathML's intent is focused more on presentation and document creation, whereas a proof assistant is focused on checking. In particular, Latex code has little semantic meaning. It is more focused about how the formula looks on a page.

Of course, there is a spectrum and the two can even be combined. While wome proof assistants like MetaMath provide very little pretty printing, other's like Lean have good unicode support (often borrowing LaTeX keywords) to make the code look more like mathematics. Further, I believe there are tools already (maybe for Mizar and Isabelle/Isar if I remember correctly) to export a PA proof into something more like natural language LaTeX or HTML. Also, Coq has a tool (whose name I forget) for turning Coq files into something more like HTML notebooks (not unlike Jupyter notebooks combine Python code and Markdown into a single readable code document). Moreover, there is no reason to think in the distant future that if proof assistants improve enough, everyone would write their proofs in a language which simultaneously makes a readable and publishable document along with a completely checked proof.

Specification and data transmission languages

One aspect of a proof assistant is just providing a way to write mathematics in an unambiguous way. With such a language one can completely and unambiguously write specifications (say for a computer chip), record mathematical knowledge, and record complex interactions between objects in a dataset (similar to, but beyond, how current knowledge graphs already store some first-order logic relationships between nodes in the graph). Very simple specification languages like JSON, YAML, and Protobufs are mostly for data, but with a PA's language you can add in conditions, relationships, functions, etc.

I would say this is more of a side effect of PAs than their intent, but we will see if this becomes important. Then more work might take off in this area. Also, Tom Hales and associates are working on a controlled natural language for mathematical statements. If say this controlled natural language only lets you write math statements, but not proofs (or doesn't check the proofs), is it a proof assistant? Likely not. It would say it would be something new.

Programming languages

Some may be confused by the current crop of dependent type theory (DTT) proof assistants like Coq, Agda, Lean, etc. These are interesting because DTT is intended as both a way to check proofs and as a way to write computer programs. From the abstract to Martin-Löf's 1982 paper Constructive mathematics and computer programming:

If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation [...], then it no longer seems possible to distinguish the discipline of programming from constructive mathematics. This explains why the intuitionistic theory of types [...], which was originally developed as a symbolism for the precise codification of constructive mathematics, may equally well be viewed as a programming language.

Coq, Lean, and Agda have all capitalized on this propositions-as-types correspondence but in slightly different ways. (I don't know enough Agda to say anything about it here except that Wikipedia calls Agda a programming language.) The pure programming language given by intentional type theory has a major difference between other programming languages. Every function must be proved to be total, so it is impossible to write an unbounded search (such as counting the number of steps of the Collatz conjecture recurrence until one gets to 1 without proving the Collatz conjecture). Hence pure DTT is not Turing complete.

Both Coq and Lean (and likely Agda) use the ability to prove judgmental equalities like 1 + 0 = 1 by just computing (or reducing) both sides. For Coq especially this is really powerful. If I understand correctly, the 4 color theorem proof in Coq was mostly a giant definitional equality proof.

Lean 3 and Lean 4 also provide a way to make impure functions which share the same language as the pure Lean functions (including the ability to call pure functions inside impure functions). This lets one also use Lean to write regular computer code with unbounded searches, infinite loops, and possibly non-terminating recursion. As for intent, Lean 3 seems to intend that these meta functions as a meta language for, say, writing tactics. (Coq on the other hand has a separate tactic-writing meta-language different from pure Coq.) Lean 4 however intends to be a full programming language as well as a full proof assistant. As such Lean 4 also has good support for IO, hash tables, reading and writing with arrays, floating point computation, and the like. But to be clear, Lean doesn't run most of this code in the kernel, but in a VM (for Lean 3) or as compiled code (for Lean 4). In that way, it is more that Lean the programming language and Lean the proof checker are using the same syntax, but using different back ends to do the computation.

While most functional languages are not dependently typed, it is still possible to use say Scala, OCaml, or Haskell as proof checkers for propositional logic. For example, in Scala the fact that I can write a function for def foo[A, B]() : A -> B -> (A, B) with no special tricks shows that A -> B -> (A and B) is constructively provable. The issue of course is that this is not the intent of Scala. Moreover, Scala provides lots of unsafe tools like type casting, non-polymorphic handling of specific types, and unbounded recursion which would make it possible to give a program for def law_exluded_middle[A]: Or[A, A -> Empty] which compiles (although that program would likely crash if I ran it).

Other proof assistants like Isabelle also have the ability to generate code. This isn't exactly the same as a programming language, but again the boundaries are blurred.

Automated theorem provers

My understanding is that automated theorem provers (ATPs) actually came before ITPs. As the name suggests ATPs are intended for automated creation of proofs, where as ITPs are intended for interactive creation of proofs. The lines definitely get blurry here. On one hand Metamath has almost no automation. The proofs are just entered by hand. On the other hand, Isabelle's Hammer provides automation on the level of an ATP (mostly because it uses an ATP in the background). In the middle, tactic-based theorem provers like HOL-Light, HOL4, Isabelle, Lean, and Coq all allow whatever automation is in the tactics, and in many it easy to write custom tactics.

To say that ATPs have no interaction is also likely not totally true. If nothing else, some ATP users have a great skill of manipulating a problem into a form where it can be solved with an ATP. That is a form of interaction.

Also, as machining learning based AI is starting to get into the theorem proving game, they often interface with ITPs instead of ATPs. In some ways, one can view the AI agent as taking the role of the human in the human-computer interaction. Since ITPs are already interactive, they are a great starting point for the back and forth interaction that an AI agent requires. Moreover, ITPs have a large amount of human-created proof data to train from. Last, the automation needs in ITPs (like creating induction proofs, library search, or doing obvious steps) are often different from the types of proofs that a typical ATP can handle well. I wouldn't be surprised to see a "proof assistant" in the future which isn't designed at all for human assistance, but just for assisting an AI agent. (Actually I would already put toy AI theorem proving environments like INT and (the backend of) rlCOP in this category.)

Computer Algebra Systems

What distinguishes a proof assistant like Lean from computer algebra system (CAS) like Mathematica is again the intended use case. Mathematica is intended for calculating with symbolic mathematical objects. While any programming language could have a library which does this sort of thing (and Python does have a few such libraries) a CAS is specialized for this purpose with often decades of prior work put into it.

However, the trade off is that CASs are not typically built with the assurances of theorem provers. There are known bugs in these systems and often they don't generate anything resembling a proof. There have been a number of papers discussion the idea of combining the two systems, either by (1) building a CAS on top of a proof assistant or (2) interfacing the two so that a CAS proves a witness/answer/proof which can be checked by the proof assistant.

It should also be mentioned that even though, say, Lean has (1) lots of mathematical objects, and (2) a full computer language, it doesn't mean Lean has good support for the kind of computations done in CASs. The issue is many-fold, but one basic problem is that the best definition (of say a polynomial) for proving may not be the best definition for computation. This is just an engineering challenge, which could in theory be solved with enough work, but it is a challenge none-the-less.

Computer games

I don't think anyone would confuse a proof assistant for a computer game, but at the same time why not? Many computer games are puzzles. The user interacts with a puzzle environment (like in "Baba is You") and has to follow the rules to get to the desired goal. Many people have commented on the similarities, and some learning resources like the Natural Number Game are specifically build around a game mechanic to make the learning more fun. Again, it is all a matter of perspective and intent.

Ad hoc proof finding code

The first 4 color theorem proof, as well as each proof finding the highest known prime number, uses computers to find a proof. The big difference between PAs is that proof assistants are general purpose. This generality makes the proofs more likely to be correct. A good analogy is that the proof-checking kernel in a PA is more like a programming language compiler, whereas the original four color theorem computer proof is more like a bespoke program. It is rare to encounter bugs in a compiler but quite common to find bugs in a program. By moving all the important parts of the computation to a small trusted computing base, it makes proof assistants more reliable than ad hoc code which checks millions of cases.

$\endgroup$
15
  • $\begingroup$ Thanks. Glad to see someone put a stake in the ground on this. I still have to read it entirely. However, this was not what I was expecting; it is spending to much time trying to show how other programming languages are not like proof assistants. I know you know the answer and hopefully this can be molded into a better answer with some feedback if you don't mind. :) continued. $\endgroup$
    – Guy Coder
    Mar 13, 2022 at 21:04
  • $\begingroup$ I would have written an answer but just am not a fan of self answers. Some of the key points you note such as total function, proof checker, assist the user in writing proofs. checking the details of a proof, write mathematics in an unambiguous way, propositions-as-types correspondence are what I was hoping to see expounded on. Also while you have some links, I am a big fan on links answers such as these. $\endgroup$
    – Guy Coder
    Mar 13, 2022 at 21:04
  • $\begingroup$ One interesting line of thought that you seem to want to broach in the answer is how automated theory provers evolved into proof assistants, or as some here prefer, interactive theorem provers. That is one way I was thinking of answering this, but showing the pedigree of such systems and how many branch off from Automath and such. $\endgroup$
    – Guy Coder
    Mar 13, 2022 at 21:12
  • $\begingroup$ I like the part about AI and the future, that was something I hand not considered. $\endgroup$
    – Guy Coder
    Mar 13, 2022 at 21:14
  • 1
    $\begingroup$ @BruceAdams The spirit of my answer is that it is a continuum. But I would also say I think Z3 falls closer on the ATP side of the continuum. $\endgroup$
    – Jason Rute
    Jun 8, 2023 at 3:01
0
$\begingroup$

If you have a programming language, you can construct a program for a type that has no constructors. In proof assistant you cannot write a proof to fill up '0'.

In other words, inability to prove a contradiction makes a proof assistant separate from a programming language.

$\endgroup$
3
  • 1
    $\begingroup$ I hate to say I can not see myself giving this an accept vote. It has even less detail than the answers from the CS version. Upvote for answering. $\endgroup$
    – Guy Coder
    Feb 10, 2022 at 16:16
  • $\begingroup$ The totality/partiality criterion doesn't seem accurate. Much progress in functional programming has been driven by the desire to avoid partiality, culminating in the paradigm of total programming. Isabelle is built on a partial specification language proofassistants.stackexchange.com/questions/154/… although of course the proof language is consistent. There are also research projects like Zombie that seek to enable nontermination without fully compromising the type system. $\endgroup$
    – Li-yao Xia
    Feb 10, 2022 at 19:34
  • 1
    $\begingroup$ In the other direction, plenty of prototype proof assistants assume type-in-type for simplicity, thereby technically making them inconsistent. But I think any reasonable definition would still count them as proof assistants. $\endgroup$ Feb 10, 2022 at 21:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.