<p>Currently, what are the major applied focuses (if any applications can be deserved such a distinction) of different proof assistants, such as the following? If there are significant differences between each of these assistants, why?</p>

<ul>
<li>Coq</li>
<li>Isabelle</li>
<li>Mizar</li>
<li>Agda</li>
<li>NuPRL</li>
<li>any other assistants you have a lot of experience with.</li>
</ul>

<p>This may be an overly broad question for this site; in that case, this more specific question may work better: what are the strengths and weaknesses of these proof assistants for formal verification? (for example, to me intuitively the set theoretic foundation of Mizar seems like a misfit for verification, but I really don't know if this intuition is correct)</p>

<p>(I can't quite justify the broadness of the question, but here's some context: I am the most familiar with Coq and its usage in verification and formalization of mathematics, but much less so with the other assistants. So I guess I want to know what is out there. It's kind of like categorical thinking (as opposed to set theoretic thinking): an object should be characterized by how it's used rather than its extensions. Currently I know some scattered facts about each of these assistants but I really don't have an idea how they are used in practice, other than Coq.)</p>

CC BY-SA 3.0
2015-08-05T19:53:10.403Z
Would you dare to ask a similar question about the major applied focuses of different programming languages, like C#, C++, C, Java, Haskell, Common Lisp,  Standard-ML, OCaml, Python, ...? Would you start your question by saying that C# has become a popular choice, at least partly due to the two monumental works in this area, ...? I don't even want to doubt that monumental work was done for C# or Coq, but singling out a single candidate doesn't make this broad question more focused, instead it adds an opinion based touch.
Thomas Klimpel
CC BY-SA 3.0
2015-08-05T20:34:17.553Z
well, the point is that I'm not familiar enough with all of these languages to say anything about them, and hence the question. But I apologize for that first sentence. I'll edit it away.
SorcererofDM
CC BY-SA 3.0
2015-08-05T21:42:33.720Z
This could be a great question if you do not focus on the applications and instead ask what are the differences of various proof verifying *techniques* and what that entails for their usage, which seems to me that is your actual question.
chazisop
CC BY-SA 3.0
2015-08-06T07:54:51.710Z
There are some good comparison articles out there, for example: [Freek Wiedijk, Comparing mathematical provers](http://www.cs.kun.nl/~freek/comparison/diffs.pdf), or [H. Geuvers, Proof assistants: History, ideas and future](http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf)
Marzio De Biasi
CC BY-SA 3.0
2015-08-06T08:58:56.187Z
I don't think that the comparison with programming languages is valid. If you know how to program well in one language you can migrate to any other with little conceptual effort. Except maybe for paradigms declarative/functional. But knowing how to use a proof assistant is not a guarantee that you'll be able to use the others with little effort.
Mateus de Oliveira Oliveira
<soft-question><interactive-proofs><coq>
major applied focuses of different proof assistants
SorcererofDM
# major applied focuses of different proof assistants

(Asked by: username_0 on 2015-08-05)

Currently, what are the major applied focuses (if any applications can be deserved such a distinction) of different proof assistants, such as the following? If there are significant differences between each of these assistants, why?

* Coq
* Isabelle
* Mizar
* Agda
* NuPRL
* any other assistants you have a lot of experience with.

This may be an overly broad question for this site; in that case, this more specific question may work better: what are the strengths and weaknesses of these proof assistants for formal verification? (for example, to me intuitively the set theoretic foundation of Mizar seems like a misfit for verification, but I really don't know if this intuition is correct)

(I can't quite justify the broadness of the question, but here's some context: I am the most familiar with Coq and its usage in verification and formalization of mathematics, but much less so with the other assistants. So I guess I want to know what is out there. It's kind of like categorical thinking (as opposed to set theoretic thinking): an object should be characterized by how it's used rather than its extensions. Currently I know some scattered facts about each of these assistants but I really don't have an idea how they are used in practice, other than Coq.)

**Tags:** soft-question, interactive-proofs, coq

> **Comments:**
> **username_1**: Would you dare to ask a similar question about the major applied focuses of different programming languages, like C#, C++, C, Java, Haskell, Common Lisp,  Standard-ML, OCaml, Python, ...? Would you start your question by saying that C# has become a popular choice, at least partly due to the two monumental works in this area, ...? I don't even want to doubt that monumental work was done for C# or Coq, but singling out a single candidate doesn't make this broad question more focused, instead it adds an opinion based touch.  
> **username_0**: well, the point is that I'm not familiar enough with all of these languages to say anything about them, and hence the question. But I apologize for that first sentence. I'll edit it away.  
> **username_2**: This could be a great question if you do not focus on the applications and instead ask what are the differences of various proof verifying *techniques* and what that entails for their usage, which seems to me that is your actual question.  
> **username_3**: There are some good comparison articles out there, for example: [Freek Wiedijk, Comparing mathematical provers](http://www.cs.kun.nl/~freek/comparison/diffs.pdf), or [H. Geuvers, Proof assistants: History, ideas and future](http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf)  
> **username_4**: I don't think that the comparison with programming languages is valid. If you know how to program well in one language you can migrate to any other with little conceptual effort. Except maybe for paradigms declarative/functional. But knowing how to use a proof assistant is not a guarantee that you'll be able to use the others with little effort.  

---

## 0 answers

