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:
“Clay answered the petition by declaring that while he looked on the institution of slavery as an evil, it was ‘nothing in comparison with the far greater evil which would inevitably flow from a sudden and indiscriminate emancipation.’”
—State of Indiana, U.S. public relief program (1935-1943)
“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)