It's often suggested that Lean is a general programming language but I don't see typical libraries to do basic stuff in it, like an arg parser, web server, GUI, SQL integrations etc.

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

How practical is rewriting, say, grep in Lean?

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.