0
$\begingroup$

I have thought of systems like Coq & Isabelle as programming languages specialised for writing proofs. A programming language might or might not have a REPL making it interactive but the REPL is not core to its being.

There are two questions here:

From my reading of them What is a Proof Assistant? does not imply interactivity or specifically an ITP (interactive theorem prover).

What is a Proof Assistant? has three good quality answers that do not emphasize interactivity.

But the answers to what-makes-a-proof-assistant-a-proof-assistant imply it quite strongly.

The wikipedia definition of Proof_assistant strongly implies the term is synonymous with ITP

"a proof assistant or interactive theorem prover"

  1. Is a proof assistant the same thing as interactive theorem prover?

If not,

  1. what is the difference?
  2. Does it have to be interactive?

The context of this question is what is needed to move from design by contract to using a more advanced prover? (I originally wrote "proof assistant" rather than "prover") where I am thinking about proving things but not thinking about interactivity. That question might in fact be completely off topic.

Whether proof assistant means something that is intended to be interactive or something that can run unsupervised is relevant to both to whether I asked the question I intended (no - an interactive compiler would be unusual) and whether the correct question is on topic (yes - based on Are questions about automated theorem provers on topic?). It also refines the definition of proof assistant from the other two questions which I why I asked here rather than in meta.

Improve this question
$\endgroup$
5
  • 4
    $\begingroup$ I feel like this is somewhat getting into the “what is a sandwich” type of argument. As we develop newer systems, we are constantly pushing the limits and can quickly get into gray areas. But as a matter of terminology, I personally usually use “proof assistant” and “interactive theorem prover” synonymously. $\endgroup$
    – Jason Rute
    Commented Jun 8, 2023 at 18:40
  • 1
    $\begingroup$ So, would Automath, Metamath, and Mizar be considered proof assistants or not? They're not interactive, they're batch. I don't think it matters that much, to be frank. $\endgroup$
    – Alex Nelson
    Commented Jun 8, 2023 at 22:28
  • $\begingroup$ Does it really matter if it is called a proof assistant? If you would like to discuss whether something is on topic on this site, you can use the meta stackexchange. $\endgroup$
    – Trebor ♦
    Commented Jun 9, 2023 at 1:48
  • 1
    $\begingroup$ It depends what you mean by interactive. In any programming language you have to interact with the typechecker to produce a valid program, ie. if the typechecker complains and this causes you to edit your code, is this interactive? Proof assistants are no different. $\endgroup$
    – Couchy
    Commented Jun 9, 2023 at 4:26
  • $\begingroup$ Sounds to me like the answer is a clear but opinionated no then. $\endgroup$
    – Bruce Adams
    Commented Jun 9, 2023 at 11:24

2 Answers 2

Reset to default
2
$\begingroup$

It depends on what you mean by “interactive” to some extent, but the Mizar system is a command-line tool that checks proof scripts. It's definitely a proof assistant, and interacting with it consists of interactions that look rather like getting code to compile with an Ahead-of-Time compiler.

Does that sound like interactivity to you? It's certainly not a REPL. Nor indeed does Isabelle offer a REPL in any usual sense: interactions with it are typically via the Isabelle/jedit tool which is an IDE.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I've already decided based on other comments that the answer is no. I'm just waiting for the right expression of that. For the purposes of this question I count an AOT compiler as non-interactive. A REPL or an IDE is interactive by design. $\endgroup$
    – Bruce Adams
    Commented Jun 16, 2023 at 7:08
  • $\begingroup$ Actually I'll accept this for now. $\endgroup$
    – Bruce Adams
    Commented Jun 16, 2023 at 7:28
1
$\begingroup$

I agree with the sentiment that this is to some extent a "what is a sandwich?" question but here's how we define terms on the metamath home page (I thought about editing to make it less metamath specific but that seems a bit elusive, not just as a matter of terminology but even in terms of whether the operation of these systems is sufficiently similar to use common words all the time):

  • Proof assistants help you interactively create proofs.
  • Verifiers verify that a database is correct - in particular, that the proofs in a database are correct. There are over a dozen verifiers available. Metamath verifiers do not make logical inferences; they just verify that the proof as stated is correct.
  • Support and other tools perform other Metamath-related tasks. Some of these tools are also proof assistants and/or verifiers. For example, the original metamath-exe tool is a proof assistant, a verifier, and also provides various support functions such as generating HTML pages. Metamath-knife is a fast verifier in Rust that also has other capabilities. For more information, see the list of other tools for Metamath.
Improve this answer
$\endgroup$

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