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?
- 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.)