How can halting problem exist practically? Lately I learned that Adam Yedidia and Scott Aaronson showed a Turing Machine that would only stop if ZFC is consistent (Scott Aaronson blog), therefore proving that for this Turing Machine it is unprovable under ZFC whether it would stop.
I don't understand how is that possible, that we would have a concrete example of a program for which we can't say if it will stop in finite time. We surely can run this program. If it would stop after N steps, we would know it does stop and it wouldn't be undecidable. So it can't stop after N steps, for any natural N. But then it wouldn't ever stop and again, it wouldn't be undecidable.
Can you point me, where I'm wrong?
 A: You are missing a key assumption - that ZFC is an appropriately nice theory. In particular, the statement

therefore proving that for this Turing Machine it is unprovable under ZFC whether it would stop

is incorrect: all we can conclude is that if ZFC is consistent then ZFC can't prove that it doesn't halt, and if ZFC is arithmetically sound (see below) then ZFC can't prove that it does halt. But the point is, we need assumptions on ZFC in order to conclude anything about the behavior of the machine.

In more detail:
Essentially, what the machine in question does is the following: search through all possible proofs of "$0=1$" from the ZFC axioms, and halt when, and only when, it finds one. Thus:


*

*If ZFC is consistent, the machine never halts (it never finds a proof of $0=1$, since there isn't one).

*If ZFC is consistent, then - by Goedel's Second Incompleteness Theorem - ZFC can't prove that ZFC is consistent, so - while for each $N$, ZFC can prove "The machine doesn't halt in $N$ steps" - it can't prove "The machine never halts."

*So this proves: "If ZFC is consistent, then - while the machine never halts - ZFC can't prove that the machine never halts." If, in addition, we assume ZFC is arithmetically sound (that is, doesn't prove any false statements about arithmetic - this is actually vastly more than we need, but oh well), then ZFC can't prove "The machine does halt", since that would (under these assumptions) be a false statement. (Note that there are, in fact, consistent theories which prove themselves to be inconsistent!)

*So to recap, we can prove (in ZFC, or indeed much less):


*

*If ZFC is consistent, then ZFC doesn't prove "The machine doesn't halt," even though the machine truly doesn'thalt.

*If ZFC is arithmetically sound (a stronger condition than mere consistency), then ZFC doesn't decide the question "Does the machine halt?" either way.
Now the key point is that in each case we have an important assumption about ZFC: consistency, or arithmetic soundness. In general, the argument

If it would stop after N steps, we would know it does stop and it wouldn't be undecidable. So it can't stop after N steps, for any natural N.

isn't right: ZFC doesn't know that the question is undecidable, it just knows that it's undecidable if ZFC itself has a nice property. Think about the similar issue of consistency: if ZFC were inconsistent, then we would know that, so the inconsistency of ZFC would be provable in ZFC. But this isn't a contradiction, since we never proved "ZFC doesn't decide its own consistency," we just proved "If ZFC is arithmetically sound then ZFC doesn't prove its own consistency."
