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.
The proof for the undecidability of the General Halting problem does not depend on the infiniteness of the state space, tape, input, symbol set, or any other component of the Turing machines for which it holds.
What you seem to be saying is that you can write a program P on your finite machine that will take any program as input and return whether that program halts or not within a finite amount of time.
If this were possible, I could write a program that calls P on itself, then loop forever if P returns true or exit if P returns false. This contradicts P, therefore P cannot exist.
If you're willing to allow that P may sometimes not halt, then you've gotten nowhere. That P is easy - simply run the program given as input and return true if it halts. If the program doesn't halt, then neither does P.
Slashdot Mirror
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.
What you seem to be saying is that you can write a program P on your finite machine that will take any program as input and return whether that program halts or not within a finite amount of time.
If this were possible, I could write a program that calls P on itself, then loop forever if P returns true or exit if P returns false. This contradicts P, therefore P cannot exist.
If you're willing to allow that P may sometimes not halt, then you've gotten nowhere. That P is easy - simply run the program given as input and return true if it halts. If the program doesn't halt, then neither does P.