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.