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:
“I have travelled a good deal in Concord; and everywhere, in shops, and offices, and fields, the inhabitants have appeared to me to be doing penance in a thousand remarkable ways.... The twelve labors of Hercules were trifling in comparison with those which my neighbors have undertaken; for they were only twelve, and had an end; but I could never see that these men slew or captured any monster or finished any labor.”
—Henry David Thoreau (1817–1862)
“When we reflect on our past sentiments and affections, our thought is a faithful mirror, and copies its objects truly; but the colours which it employs are faint and dull, in comparison of those in which our original perceptions were clothed.”
—David Hume (1711–1776)
“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)