I know this is true:

> given any type system / proof system for correctness, there will be well behaved programs that cannot be proven correct in the proof system

But I'm not sure if this is as well:

> nor can they be refactored to equivalent programs that can be proven correct

If so, then there will be some programs whose behavior simply cannot be proven by a type system. Though I wonder if for those programs there could be another type system that could prove it? So maybe with a combination of type systems it can still be achieved?

Either way, what I meant to say was that even for programs that can, the problem of "bugs in a program" has not been completely solved. Since there can be bugs in your proof, and there are often missing assertions in it as well, in that you'll generally prove a property of it, but not directly assert precisely what you expect of each and every inputs, and you might also simply forget to prove certain key properties.