> Proving correctness is crucial in large systems.
It could be good in smaller, but critical and widely used utilities like SSH and terminals.
Yeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.
It should be feasible to rewrite the coreitils like ls, cd and cp in Lean 4 together with Cursor within days. Rsync and ssh are more complex though.
Your first claim is actually a very solid test for AI. We should start seeing a lot more AI powered OSS projects or at least contributions if AI truly is as good as they say. Heck, OSS should accelerate exponentially since contributions should become very easy.