I shouldn't have been surprised, because that part of macro writing is purely mechanical syntax transformation—just a "take these tokens and return those tokens" function that one should expect LLMs to be good at. But I was surprised, because for me that was always the hard part.
So now I can think up new macros to abstract over patterns in my code—the part of macro-writing that I enjoy—and then push a magic "implement this" button to make it work.
What I'm not sure of yet is whether this is an evolutionary dead end—a train stop on the way to "you'll never look at code again, so what does it matter what programming language you used to use". Yes, I still look at my code, and this is a pretty nice train stop, wherever the tracks lead to.
Can lean generate small static binaries the same way Go/Rust/C/C++ can?
How practical is rewriting, say, grep in Lean?
> 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.
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.