RFC: replace current kernel with lean4lean kernel / reimplement kernel in lean

[srghma]

Proposal

lets replace c++ kernel with https://github.com/digama0/lean4lean

Community Feedback

1. "How long do you think it would take someone to write a Lean type checker from scratch?"
2. Lean4Lean: Lean 4 kernel in Lean topic

[nomeata]

Thanks for trying to make lean better. I'm unsure though, how the proposed change would do that, maybe a motivation section is needed? (But overall i wouldn't recommend spending a lot of time on this, I don't expect this RFC will bring to light much that isn't known already, and I don't expect any significant short term benefits that would justify working on this in the near future.)

[srghma]

motivation:

1. @digama0 said 01:00:59 --> 01:01:07 proofs kernel is still in correct implementation, point is that it makes it easier to make correct changes, right now making correct changes requires PhD
2. @rish987 said I want to compile lean, coq, agda, isabel to common intermediate language
3. How to fix: implement kernel on lean using lean4lean, add checks, implement optimizations aka more reduction rules, checks should still work
4. lean4lean compiles metalib in 31 minutes, compared to 21 minutes from the C++ kernel, but it will claw back all performance (P.S. by the way, idris2 has a new kernel called yaffle, maybe can borrow some ideas for optimizations)
5. easier to make lean on other languages, e.g. lean completely with java instead of c++ (idris2 allows different backends, bc is compeletely written on idris2, just plug ffi)
6. rewrite EVERYTHING, even scripts like this shell.cpp with lean
7. use lean to bootstrap other new languages

[Kha]

Thanks for the additional references. As has been mentioned, we cannot justify working on this for the foreseeable future.

[srghma]

and if someone else will do it - will be accepted?

[nomeata]

No

[srghma]

but the quality of lean language will be better

[nomeata]

That’s very debatable; the quality of the lean language is totally unaffected, users do not care how the lean kernel is implemented. (Usually they don’t even care if it exists, if the rest of the system does it’s job well.)

Maybe there is a point to be made that the lean implentation is in some way better, but we don’t see how that improvement can be in near as significant as all the other things that we want to improve. So in order to avoid this distraction, we actively want to discourage anyone from working on this.

What we do do encourage people to work on is of course external checkers. Let there be many! And who knows what happens if someone exhibits a lean kernel that’s clearly superior to the existing one; faster, simpler, more trustworthy. But that is better done externally, and until then I don’t think there is anything to discuss here.