[reuben364]

While Lean4 is meant to be much more of a general purpose language than it's predecessor, it is still built with being a proof assistant in mind. That being said it is self hosted and has been in development and use for quite some time, which says something of it's readiness.

Tooling around it great (it is installed with a rustup fork called elan).

As far as performance, it uses a particular version of ref-counting that allows mutation of unique references based on run-time tracking rather than compile time. If you accidentally keep a reference to an array and modify it, then you end up copying it rather than just mutating it.