3 ms·
> Proving correctness is crucial in large systems. It could be good in smaller, but critical and widely used utilities like SSH and terminals.
by skydhash 1y ago
> Proving correctness is crucial in large systems.
It could be good in smaller, but critical and widely used utilities like SSH and terminals.
- oblio 1y agoYeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.
- rthnbgrredf 1y agoIt 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.
- oblio 1y agoYour 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.