I feel like leaving it to decide everything would not produce a good end product. It feels like just having it decide how GC should work, how the function call stack should work or any of these rather simple but actually requiring lots of decision and thinking how things fit together (and pick a good solution out of many seemingly good solutions that can come back to bite you), couple this with the tendency for AI agents to tend towards adding new code and building over features I don't think you end up with a good solution.
On formal verification having done it only in an academic sense and looked over at projects like seL4 and quite interested in that project. It feels like actually proving useful properties of programs for real programs even ones with well defined domains and easier to model such as interpreters or compilers it seems that it will just prove theorems about properties that hardly matter or don't even matter at all. See how bad it still tends to be when trying to get it to write tests.
I would be interested to know if their has been an agent that has actually utilized formal methods such as Lean or Coq or Isabella to prove properties of programs in an automated way as you suggest, I have only seen it proving mathematics and or searching for counter examples, not writing Curry-Howard style proofs.
Shoutout to Toph https://x.com/VictorTaelin who's been building a programming language out of formal method Lean proof checkers, which probably would indeed have the scope you're looking for.
I do think the current state of the AI just using rigorous tests and rendering inspection loops is still far more than most programmers did for the majority of apps, but yes I think rigorous formal verification will come too. Worst case it's gonna be something like a MechanicalTurk pipeline having us humans verify narrowed scopes the AI can't confidently inspect (yet. while also training on those results for next iteration)
As for the decision stack of what makes a good end product - turtles all the way up/down. The ProductOwnerAI role decides those things, and it will likely do so with the same deep skill that programming AIs are currently hitting our profession with. Optimizing enormous breadths of concerns and simulating results is AI's main specialty.
More precisely, a "perfect solution" doesn't exist. It's all tradeoffs given your goals. Someone needs to make the decision: 1. which tradeoffs are worth given your goals 2. which goals are worth defining or redefining. And do that effectively, you need to understand the problem, which goes back to engineering.
On formal verification having done it only in an academic sense and looked over at projects like seL4 and quite interested in that project. It feels like actually proving useful properties of programs for real programs even ones with well defined domains and easier to model such as interpreters or compilers it seems that it will just prove theorems about properties that hardly matter or don't even matter at all. See how bad it still tends to be when trying to get it to write tests.
I would be interested to know if their has been an agent that has actually utilized formal methods such as Lean or Coq or Isabella to prove properties of programs in an automated way as you suggest, I have only seen it proving mathematics and or searching for counter examples, not writing Curry-Howard style proofs.