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.