I am currently working on a language compiler in lean and it seems to be fine, but compilation times are horrific and having a mathlib dependency just to build a programming language is a big ask for people.
OTOH, my borrow checker is provably sound, which is why I am using it.
OTOH, my borrow checker is provably sound, which is why I am using it.