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.