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 typ

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.