[nightski]

Most software problems I encounter in the real world ARE of bounded complexity, and they can be reduced to software verification. But this is still a very tedious process and there are significant gains to be had by making this more accessible without having to solve the hardest problem in computer science.

[pron]

Certainly. It's just that there cannot be one (or a few) advances that would make writing correct programs generally easy. We can concentrate on domains (in the safety-critical embedded world this is almost a solved problem for some kinds of applications thanks to the invention of synchronous languages in the '80s, that make formal verification relatively efficient). We can also address some "internal" properties, like memory safety and transactions, that on the whole might make writing correct programs easier (though not provably correct).