You can look forward to that, but today I’m already experiencing something worse but close enough for all but the most critical code: AI-driven algorithm design

You can look forward to that, but today I’m already experiencing something worse but close enough for all but the most critical code: AI-driven algorithm design + tests in your favorite property-based testing library (like OG QuickCheck in Haskell or hypothesis in Python). Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.