This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits in N bytes.

If you remove infinite tape, you go from undecidable to "just" exponentially complex.

> If you remove infinite tape, you go from undecidable to "just" exponentially complex.

Which is a huge leap - we got from "impossible" to "possible in principle" and we now can do research how to make it even "sufficiently fast" for problems of practical relevance.

No. In CIC I can prove that, say, some property is valid for _any_ natural number. Your "memory is bounded" argument is invalid, as formal proofs can go beyond that.

...Also I think you don't realize that formal inductive proofs can easily reason about programs operating with unbounded memory.

With formal inductive proofs, you can reason, but not decide.

Does the proof that the halting problem is not solvable actually make use of the unboundedness of the tape?

Standard proof is a diagonalization, which depends on infinite sequences.

That said, the Halting problem on physical computers is still of extremely high computational complexity, which can be just as high a barrier as incomputability.

Of course it does (implicitly!).

Otherwise the number of possible states of the Turing machine T that we want to check whether it halts or not is finite and we just have to "simulate" the program and see whether it terminates or it reaches again a state that it was already in.

How would the "if this program halts then run forever, else halt" algorithm work on a real computer? I imagine it would fail with stack overflow.