Building a suite of libraries for basic stuff like webserver, sql integration, writing react components etc in Lean here https://github.com/orgs/theoriclabs/repositories?q=sort%3Ast...

> Can lean generate small static binaries the same way Go/Rust/C/C++ can?

Lean compiles to C and the binaries aren't huge, though haven't benchmarked this part yet.

> How practical is rewriting, say, grep in Lean?

Very, you should probably try it.

a mathematician friend of mine has been building a game engine with it. very neat stuff, anything is possible!

Lean compiles its code to C, so it's pretty good on that end of the spectrum, though it does have a bit of a runtime, so it's certainly not at the very end of spectrum where Rust/C/C++ are (never used Go, so idk). With some optimization my personal experience is that it's not that bad to get it within a factor of 2-5 of half-decent rust speed. My personal mental model of it is like a more-to-my-tastes wildly-faster python but without an ecosystem.

As for library support, yeah it's definitely not a mature ecosystem. But since it compiles to C, the FFI is great, so you can just ask an LLM to write bindings to your favorite rust/C/C++ library and they do just fine. I recently wanted (apache) arrow bindings for lean, and LLMs knocked out perfectly sufficient bindings just fine.