> 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 :)