What you say is possible, and my knowledge stops short of it. I know this is true: > given any type system / proof system for correctness, there will be well

What you say is possible, and my knowledge stops short of it. 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.