Re:Verifying compiler? Correctness proving tools? (Score 2, Interesting)

You're right. We can't write a program that takes any program as input and returns whether or not it halts in finite time.

We also can't write a program that verifies whether or not a given theorem in a sufficiently powerful formal system is true. This doesn't seem to stop us from doing math, or even writing theorem provers.

There are many, many programs about which we can programmatically verify generally undecidable properties. And if we can't for a given input, we can either disallow it as input, recognize it and give up, or just let our program loop merrily. In fact, I would be surprised if there is a real-world program out there now or in the future that can't written so that it can be be verified to halt or not. Has anybody been stopped from necessary computation by Post's Correspondence Problem? Doubtful.

There is a whole field of creating these types of compilers known as Proof Carrying Code. The idea is that a user specifies a security policy detailing what properties a program needs (halts, memory-safe), then a compiler automatically supplies and bundles with the code a proof if one exists, which is then verified before the program is run. This is real technology that works on large classes of real programs.