Code generation should be relatively straightforward with language model. Start with a problem description and let the LLM generate the code. It should be fairly simple to ask for a proof of correctness for the generated code, then verify that proof (for instance by creating property-based tests), and finally ask for a human-readable summary of the proof. Pass this to human code review and you have a pretty good code generation machine. Failure at any step can simply lead to another iteration.

The thing is: SE doesn't work like this anymore. People aren't used to formalized requirements and take 99% just for granted. (Which web developer really takes network errors into account nowadays?).

With "AI" we might have the tools we need to really solve the software crisis.