Earlier quoted context omitted.
Provable code would solve the root cause, yes. :) However, even with provable code, the proof actually has to be both correct and performed. There are too many competing factors that won't allow idris, for example, to actually work. The result is that, as an industry, the Internet and the world's business are held together by twine, twist ties, and spaghetti code. Even this very webpage is just enough to work for mos…
so... I guess strong-AI-based coding is the only 100% sure way to go (but... I'd be jobless if that were to happen :(
The terms are somewhat contentious, but AIs are more prone to use heuristics than traditional algorithms, which would add another layer of complexity.
So, we can't be certain that such an AI itself wouldn't create bugs. If anything, it would be easier to show that bugs would get created.
This is simply the state of software. We all deal with it in the ways we can, trying our best to minimize issues and add value.