Thankfully correctness in the general case doesn't matter in reality, in the same way that it doesn't matter that not all 'correct' programs can be possibly typed.

And I don't know why you put "prove" in scare quotes. There is formally verified software that has been proven to conform to a spec. They aren't just toy programs either, see SEL4 or CompCert for 'real' programs.

The halting problem doesn't prevent you from writing proofs for programs, same as Gödel's theorems don't prevent mathematical proofs from existing.

Fully verified programs do exist (e.g. CompCert C compiler), although for various reasons, it's still a niche.

> Proofing correctness (in general) is incomputible (halting problem and stuffs).

> Those "prove" you see in academic paper are very specific case.

Not to put too fine a point on it, but every program written is a very specific case, so I'm not sure this is such a convincing point.

As you say, there is absolutely, provably, no general-purpose algorithm out there that will prove program correctness automatically. That is in no way to say that humans can't or shouldn't try to prove some programs correct, or even that you can't have an algorithm that will prove certain classes of programs correct.

With that said, I do also think your parent:

> We have figured it out. People with a PhD and given enough time can do it. Scaling this will be possible, especially with the help of AI, as soon as there is the actual will there to do it.

is too optimistic, and throwing a little cold water on that rosy prediction is appropriate.