What few people realize, is that most completely arbitrary programs are very uninteresting. More interesting programs have characteristics that would very often allow to statically prove that all of their loops that should terminate indeed will terminate. And even interesting loops for which it would not be in the first time possible to determine that often gain in clarity from being slightly changed so that the tool can do its work.

IIRC MS has a tool that does sort of that for windows drivers.

It is easily provable that this is theoretically possible, but the required time is too long for it to be applicable. Suppose your memory has N states. Run your program through N+1 computation steps and if it's not already finished, then it will never halt.

Thing is, N is very large for real memory, so this straightforward approach is not applicable. However, there's much room to improve this algorithm and I assume that's what the MIT folks did.

True halting problem is about computational devices with infinite memory.

Let's consider both computers (yours and 3rd party) as a single computational device, with a state represented by a pair of symbols, where the first represents your computer and the second the 3rd party's. Suppose your computer has N states and the other M. It's enough to run N * M + 1 computation steps -- if your program hasn't ended so far, it will never, for there's a certain state (a, b) that must have occured twice, by the pigeonhole principle.

Please keep in mind that this is all purely theoretical, and not at all practical. It's just a counterargument to other purely theoretical argument from unsolvability of halting problem.

  def is_collatz(n):
   s = set()
   while n not in (1, 2, 4):
    if n % 2:
     n = 3 * n + 1
    else:
     n /= 2
    if n in s: # Non-Collatz loop
     return False
    s.add(n)
   return True

Secondly, you're making the logic error A => B implies not A => not B. If state spaces as large as modern memory limits allow are too large, that doesn't imply that state spaces far below modern memory limits are small enough to handle.

Thirdly, your program trivially terminates doing nothing.

Pretend that an OOM condition is the same as a False answer. :3

Here's a program, building on the previous one, which either terminates or doesn't.

  from itertools import count
  for i in count(1):
   if not is_collatz(i):
    break

I can tell you now that your code terminates. The set s is strictly increasing in size, inevitably going towards an OOM condition if the loop doesn't terminate by other means. Note that we are talking about determining halting or not halting, not with which value the program halts.

This is not a troll. You tried to respond with something witty. I just pointed out that in this case things like the collatz conjecture don't apply, because it is a conjecture over all natural numbers. When you are working with finite memory, there is no way to encode this conjecture into a program (e.g. by making it halt if the conjecture is true and making it loop when the conjecture is false).

Real-life computers have bounded memory, so they don't have any more computational power than, say, regular expressions matchers -- every computational task performed by real computer can be represented by appropriately complicated regular expression. That's why one needs to be especially careful when arguing from computability when talking about real-life problems.

The more serious issue is a treatment of I/O.