Comparison
See also: Proof assistant#Comparison| Language | Actively developed | Paradigm | Tactics | Proof terms | Termination checking | Types can depend on | Universes | Proof irrelevance | Program extraction | Extraction erases irrelevant terms |
|---|---|---|---|---|---|---|---|---|---|---|
| Agda | Yes | Purely functional | Few/limited | Yes | Yes (optional) | Any term | Yes (optional) | Proof-irrelevant arguments (experimental) | Haskell, Javascript | Yes |
| ATS | Yes | Functional / imperative | No | Yes | Yes | ? | ? | ? | Yes | ? |
| Cayenne | No | Purely functional | No | Yes | No | Any term | No | No | ? | ? |
| Coq | Yes | Purely functional | Yes | Yes | Yes | Any term | Yes | No | Haskell, Scheme and OCaml | Yes |
| Dependent ML | No | ? | ? | Yes | ? | Natural numbers | ? | ? | ? | ? |
| Epigram 2 | Yes | Purely functional | No | Coming soon | By construction | Any term | Coming soon | Coming soon | Coming soon | Coming soon |
| Guru | Yes | Purely functional | hypjoin | Yes | Yes | Any term | No | Yes | Carraway | Yes |
| Idris | Yes | Purely functional | Yes | Yes | Coming soon | Any term | No | No | Yes | Yes, aggressively |
| Matita | Yes | Purely functional | Yes | Yes | Yes | Any term | Yes | ? | OCaml | ? |
| NuPRL | No | Purely functional | Yes | Yes | Yes | Any term | Yes | ? | Yes | ? |
| PVS | Yes | ? | Yes | ? | ? | ? | ? | ? | ? | ? |
| Typed Racket | Yes | No | ? | ? | ? | ? | ? | ? | ? | ? |
| Sage | ? | Hybrid typechecking | ? | ? | ? | ? | ? | ? | ? | ? |
| Twelf | Yes | Logic programming | ? | Yes | Yes (optional) | Any (LF) term | No | No | ? | ? |
| Xanadu | No | Imperative | ? | ? | ? | ? | ? | ? | ? | ? |
Read more about this topic: Dependent Type
Famous quotes containing the word comparison:
“[Girls] study under the paralyzing idea that their acquirements cannot be brought into practical use. They may subserve the purposes of promoting individual domestic pleasure and social enjoyment in conversation, but what are they in comparison with the grand stimulation of independence and self- reliance, of the capability of contributing to the comfort and happiness of those whom they love as their own souls?”
—Sarah M. Grimke (1792–1873)
“From top to bottom of the ladder, greed is aroused without knowing where to find ultimate foothold. Nothing can calm it, since its goal is far beyond all it can attain. Reality seems valueless by comparison with the dreams of fevered imaginations; reality is therefore abandoned.”
—Emile Durkheim (1858–1917)
“We teach boys to be such men as we are. We do not teach them to aspire to be all they can. We do not give them a training as if we believed in their noble nature. We scarce educate their bodies. We do not train the eye and the hand. We exercise their understandings to the apprehension and comparison of some facts, to a skill in numbers, in words; we aim to make accountants, attorneys, engineers; but not to make able, earnest, great- hearted men.”
—Ralph Waldo Emerson (1803–1882)