Timeline for Proof Assistants in OOP languages
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20 at 10:21 | comment | added | Meven Lennon-Bertrand♦ | Re the right tool for the job: it is not just parsers and interpreters, a lot of what happens in proof assistant implementation is manipulation of very structured data, aka algebraic datatypes, such as ASTs. These constructs were historically only available in functional languages (along with good pattern-matching, which is necessary to manipulate these structures easily). | |
| Feb 19 at 23:00 | comment | added | Michael Norrish | Great answer! But, strictly, the prover we run on top of CakeML (which we call Candle) is based on HOL Light. And that version of the kernel is verified to the extent that Gödel's theorem permits. The tower is thus: SML (poly/ml) / HOL4 / CakeML / Candle (HOL Light-ish) | |
| Feb 15 at 17:43 | vote | accept | Kid A | ||
| Feb 14 at 11:53 | history | answered | Jason Rute | CC BY-SA 4.0 |