The halting problem doesn't prevent correctness proofs, it only means that you get a three-valued answer: proof, counterexample, or too complex to determine. "T

The halting problem doesn't prevent correctness proofs, it only means that you get a three-valued answer: proof, counterexample, or too complex to determine. "Too complex to determine" usually means that the code needs to be rewritten to have simpler structure. And of course the proof is only for those properties that you write down, and you could also have a bug in the spec for those properties.