Hacker News new | ask | show | jobs
by digama0 2052 days ago
> implementation in C++ rather than a nice functional language for dogfooding

To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure functional) language. The siren song is strong :)

1 comments

Oh, I did not know that! Will check it out.