It's really incredible. We decided to see if we could write a Tokio-like library in Lean and were able to do it in a week with performance similar to Node 22. There is really no reason not to use a theorem prover now instead of a functional programming language, and soon it will be better than most languages. All that will remain that it can't do are the jobs of low level languages like C++ [for now].