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.

Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself.

Now it has a RC GC and boxes everything >= 64 bits (including struct fields and IO/ST results), and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago).

[1] https://github.com/kmill/lean4-raytracer