4 ms·

Checkout Lean, the lead developer also started Z3 . Lean 3 is implemented in C++ and apparently is much faster than Coq. They are in the process of implementing

Checkout Lean, the lead developer also started Z3 . Lean 3 is implemented in C++ and apparently is much faster than Coq. They are in the process of implementing Lean 4, which will feature native code generation and might become one of the first practical dependently typed programming languages.

h91wka 6y ago
Lean 3 is community maintained, aka dead. Lean 4 is described as "go away", and it will be incompatible with Lean 3. So much for practicality.
tom_mellior 6y ago
> Lean 3 is implemented in C++ and apparently is much faster than Coq. 1. The parent didn't comment in any way on Coq's performance, they barely mentioned Coq at all. 2. Coq is implemented in OCaml, which produces pretty good code. If Lean is faster than Coq, that's more likely due to more optimized algorithms or data structures. 3. Your wording using "apparently" suggests that you don't even have practical experience with this, you just want to promote a software system you have never used? What is the point of a comment like this?