Lean can be used to write software in [0]. I dare say that it may even be the intended use for Lean 4. Work on porting mathlib to Lean 4 is far along and the ma

Lean can be used to write software in [0]. I dare say that it may even be the intended use for Lean 4. Work on porting mathlib to Lean 4 is far along and the mathematicians using it will certainly continue to do so. However there is more space for software written in Lean 4 as well. However... it's no where near ready for production use. They don't care about maintaining backwards compatibility. They are more focused on getting the language itself right than they are about helping people build and maintain software written in it. At least for the foreseeable future. If you do build things in it you're working on shifting ground. But it has a lot of potential. The C code generated by Lean 4 is good. Although, that's another trade-off: compiling to C is another source of "quirks." [0] https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/