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.
I guess that's the true Turing Test, can an artificial general intelligence determine the complexity level and relative risk level of infinite loops for an algorithm written for a Turing machine.
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.