> Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability.
Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways:
1. The tool crashes a lot
This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++.
2. You don't feel safe trusting it when it says it proves something
Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of universes, and there exist independent typecheckers written in Haskell <https://github.com/leanprover/tc> and Scala <https://github.com/gebner/trepplein>. I have an in-progress one written in Rust as well.
Meanwhile, Lean is quite fast, the metaprogramming is lovely, and there are some really awesome tools in the pipeline.
For how long this will last? Many will agree here, that C++
is known for its ineptitude for "long-term" projects where maintenance issues are of crucial importance. I presume that proof assistants belong to that class. If Leo is the only developer of this project for the rest of life, then it is OK, I guess.
That's a reasonable concern. If Leo got hit by a bus the code quality would certainly suffer. He's pretty good about cleaning up PRs etc after merge, by which I mean, even if he isn't the only developer right now he does a lot of work to make sure the C++ code is up to snuff.
Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways:
1. The tool crashes a lot
This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++.
2. You don't feel safe trusting it when it says it proves something
Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of universes, and there exist independent typecheckers written in Haskell <https://github.com/leanprover/tc> and Scala <https://github.com/gebner/trepplein>. I have an in-progress one written in Rust as well.
Meanwhile, Lean is quite fast, the metaprogramming is lovely, and there are some really awesome tools in the pipeline.