Timeline for Proof Assistants in OOP languages
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 15 at 15:29 | comment | added | Alex Nelson | @KidA The only real "difficulty" is that object-oriented programs tend to be difficult to "reason about". Functional languages are far easier in this regard, which is probably one more reason why most proof assistants are written in functional languages. Jason Rute's answer gives more reasons why functional languages may be preferable. | |
| Feb 13 at 16:26 | comment | added | Alex Nelson | @AndrejBauer There's no truth in advertisement anymore :( The kernel is entirely C++. | |
| Feb 13 at 13:24 | comment | added | Jason Rute | Also my understanding is that to build Lean 4 there is a bootstrap of Lean 4 written in C++ so that you can then build Lean 4 in the C++ implemented bootstrap of Lean 4. So in that sense you could also say Lean 4 is also written in C++. | |
| Feb 13 at 13:15 | comment | added | Jason Rute | @AndrejBauer Most of Lean 4 is implemented in Lean 4, including the language server, parser, elaborator, and tactics. See here.. The logical kernel is still in C++, as is the interpreter which runs non-compiled Lean code. (The compiler uses Lean 4 to compile to C as an intermediate language and then to byte code.) There is an alternate Lean 4 checker Lean4Lean written in pure Lean 4, which could be a kernel. It is slower but it’s in pure Lean so can in the future be proved correct which is exciting. | |
| Feb 13 at 9:34 | comment | added | Andrej Bauer | The ads say Lean 4 is implemented in Lean 4, so what's up with that? | |
| Feb 13 at 8:11 | comment | added | Kid A | Thank you. So there's no mathematical inconsistency, programmatic errors that would appear in oop programming languages... I want to use Kotlin as the main language. | |
| Feb 12 at 23:09 | history | answered | Alex Nelson | CC BY-SA 4.0 |