> First, the halting problem only applies to systems with infinite memory. If memory is finite and the system is deterministic, the program will either halt or

> First, the halting problem only applies to systems with infinite memory. If memory is finite and the system is deterministic, the program will either halt or repeat a state. The halting problem is thus decidable for non-infinite systems. So there. The article mentions this fact specifically in about the third paragraph, and goes on to talk about why it's less relevant than it might appear. > The next question is whether there are programs with lower time bounds that can be made arbitrarily large. Actually, we don't know the answer to that. No, the time hierarchy theorems prove that such programs exist. > My usual comment on this is that if your program is unreasonably hard to test for termination, it's broken. Microsoft takes that position with their Static Driver Verifier. There's a timeout; if it takes too long to prove your kernel driver safe, it doesn't get signed for use in the kernel. Timeouts make it much harder to reason about programs and perform safe refactors, because the class of refactors that are guaranteed to not break a program becomes quite small. E.g. you can no longer prove that "val y = f(x); g(y)" is correct if "g(f(x))" is correct and vice versa.