[unboxed_type]

I agree with most things you said, however.

> Lean is written in pretty principled C++.

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.

[cmrx64]

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.