> ... because computers aren't Turing machines and have finite memory, so all programs are guaranteed to halt.
Is this simply wrong or am I not understanding? With finite memory, the halting problem is solvable, but that's different than all programs halt.
while True:
pass
The program doesn't halt even with finite memory. Unless he means eventually the world will end, or the power supply will die, etc.
> If the halting problem was solvable, then anyone with a computer could prove Goldbach's conjecture in an afternoon.
Why does he say "in an afternoon"? Maybe it would take 10^100 years? The halting problem be solvable or unsolvable is not a question of complexity or efficiency.
Someone discovered the halting problem again. Sigh.
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 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. Cryptography assumes the answer is yes, but that's an assumption. We don't actually know that factoring is inherently hard, only that enough people have beaten on the problem that we know there's no easy to find shortcut.
Proof of correctness systems run into the complexity problem. You can write things that force a SAT solver to explore so many cases that it won't finish in any reasonable time. But that's not undecidability. 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.
> A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point
Penrose comes to mind. There are people who are desperate to prove that humans transcend computers in some fundamental way. We heard a lot more from that crowd before LLMs started writing better than some of their critics.
This is a rant I’ve had in my head forever, so thanks for posting this. A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point, like this one. But the actual proof is so disappointing and non-philosophical that I wonder if anyone making these grand statements has ever read it. It just invents a program which outwits the halting detector by doing the opposite of what it would otherwise say.
Its like, if you met the smartest person in the world, and you asked them “will you answer no to this question” and then no matter what they said you laughed in their face and said hah, guess you’re not so smart, are you?
And THAT is why you think we don’t live in heaven?
Like, OP says that because of this proof we can’t run HALT() on a program that assets the Goldbach conjecture. What? That’s entirely orthogonal from the proof of the undecidability of the halting program, unless one of the primes has embedded a trick logic question into itself somehow. There’s nothing stopping there from being a “HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM”. There you go, you’re back in heaven again!
The following argument from the blog post is wrong:
"First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run P1, just call HALTS(P1, Solver) to see if the solver solves all problems in polynomial time."
The difficulty here is that it could turn out that there's a SAT algorithm that is better than exponential, but the SAT solver used in the experiment does have worst case exponential time. What has to be proved, to prove P != NP, is that there is no possible SAT algorithm that has sub-exponential worst case time.
If the halting problem were decidable, we wouldn't need to rewrite the world in Rust; we could write a checker for C that would anticipate all memory safety violations of an arbitrary C program at compile time.
The gist of the article is of course correct, but it uses some terminology wrong. "Recursively enumerable" and "decidable" aren't applicable to instances of individual programs. In fact, every single instance of a problem is "decidable" because either the program that always returns true or the one that always returns false solves it (we don't necessarily know which one, but that isn't required). And in any case, for the Goldbach conjecture, the set of numbers that satisfy it is decidable - the function sum_of_two_primes is such a decision procedure.
What's undecidable is the set of valid conclusions (from some axioms) in first-order logic (in short, "FOL is undecidable"). So there is no algorithm that can tell us whether a given mathematical statement (including Goldbach's conjecture) is "true" (i.e. follows from the axioms of arithmetic, or ZFC, or something). FOL is recursively enumerable, since we can just generate all possible proofs.
Similarly, the set of halting programs isn't decidable, but it is recursively enumerable (every halting program halts at some time t, now enumerate all pairs (program, t) via a diagonal argument and check if program halts within t steps).
Is it me, or does the section about the Goldbach conjecture have nothing to do with the halting problem, but with finite machines?
As TFA points out, the program to solve the Goldbach Conjecture will halt, and we know this. Because it halts, it doesn't solve the conjecture (unless it does solve it within the range of numbers allowed by the finite system memory).
So it's got nothing to do with the halting conjecture - we know this program will definitely halt, because we don't have infinite memory. It also doesn't solve the conjecture, because it will halt. This seems like circular reasoning.
If we had an infinite machine then we could write a program that could solve the conjecture, if we had infinite time to run it in (or it ran infinitely fast). Because we don't have any of those things, writing a program to solve the conjecture is impossible, regardless of our ability to determine if it halted or not.
If we had the ability to determine if that program halted, we would still need an infinite machine to run the program, which we don't, so the ability to determine whether the program halts or not is irrelevant. We can't create such a program (because we can trivially determine that any such program will actually halt - yes it does, because it runs out of memory).
Stephen Wolfram talks about computational irreducibility and I think of that as essentially the same as the halting problem. I like his description that science advances by finding problems that we care about that are also computationally reducible. An equivalent with halting is to find those problems that we care about where halting can be proven (or disproven).
The reason why the halting problem is of minor importance for pragmatically minded programmers has nothing to do with machine memory size. It's of minor importance because while it's intractably hard to prove an arbitrary program has some desired properties, it's considerably and practically easier to reliably construct a program with said properties. That problem of program construction is what we as programmers are trained and paid to do, and overall we do an adequate job of it.
> ... because computers aren't Turing machines and have finite memory, so all programs are guaranteed to halt.
Is this simply wrong or am I not understanding? With finite memory, the halting problem is solvable, but that's different than all programs halt.
The program doesn't halt even with finite memory. Unless he means eventually the world will end, or the power supply will die, etc.> If the halting problem was solvable, then anyone with a computer could prove Goldbach's conjecture in an afternoon.
Why does he say "in an afternoon"? Maybe it would take 10^100 years? The halting problem be solvable or unsolvable is not a question of complexity or efficiency.
Someone discovered the halting problem again. Sigh.
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 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. Cryptography assumes the answer is yes, but that's an assumption. We don't actually know that factoring is inherently hard, only that enough people have beaten on the problem that we know there's no easy to find shortcut.
Proof of correctness systems run into the complexity problem. You can write things that force a SAT solver to explore so many cases that it won't finish in any reasonable time. But that's not undecidability. 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.
> A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point
Penrose comes to mind. There are people who are desperate to prove that humans transcend computers in some fundamental way. We heard a lot more from that crowd before LLMs started writing better than some of their critics.
This is a rant I’ve had in my head forever, so thanks for posting this. A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point, like this one. But the actual proof is so disappointing and non-philosophical that I wonder if anyone making these grand statements has ever read it. It just invents a program which outwits the halting detector by doing the opposite of what it would otherwise say.
Its like, if you met the smartest person in the world, and you asked them “will you answer no to this question” and then no matter what they said you laughed in their face and said hah, guess you’re not so smart, are you?
And THAT is why you think we don’t live in heaven?
Like, OP says that because of this proof we can’t run HALT() on a program that assets the Goldbach conjecture. What? That’s entirely orthogonal from the proof of the undecidability of the halting program, unless one of the primes has embedded a trick logic question into itself somehow. There’s nothing stopping there from being a “HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM”. There you go, you’re back in heaven again!
The following argument from the blog post is wrong:
"First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run P1, just call HALTS(P1, Solver) to see if the solver solves all problems in polynomial time."
The difficulty here is that it could turn out that there's a SAT algorithm that is better than exponential, but the SAT solver used in the experiment does have worst case exponential time. What has to be proved, to prove P != NP, is that there is no possible SAT algorithm that has sub-exponential worst case time.
If the halting problem were decidable, we wouldn't need to rewrite the world in Rust; we could write a checker for C that would anticipate all memory safety violations of an arbitrary C program at compile time.
The gist of the article is of course correct, but it uses some terminology wrong. "Recursively enumerable" and "decidable" aren't applicable to instances of individual programs. In fact, every single instance of a problem is "decidable" because either the program that always returns true or the one that always returns false solves it (we don't necessarily know which one, but that isn't required). And in any case, for the Goldbach conjecture, the set of numbers that satisfy it is decidable - the function sum_of_two_primes is such a decision procedure.
What's undecidable is the set of valid conclusions (from some axioms) in first-order logic (in short, "FOL is undecidable"). So there is no algorithm that can tell us whether a given mathematical statement (including Goldbach's conjecture) is "true" (i.e. follows from the axioms of arithmetic, or ZFC, or something). FOL is recursively enumerable, since we can just generate all possible proofs.
Similarly, the set of halting programs isn't decidable, but it is recursively enumerable (every halting program halts at some time t, now enumerate all pairs (program, t) via a diagonal argument and check if program halts within t steps).
Is it me, or does the section about the Goldbach conjecture have nothing to do with the halting problem, but with finite machines?
As TFA points out, the program to solve the Goldbach Conjecture will halt, and we know this. Because it halts, it doesn't solve the conjecture (unless it does solve it within the range of numbers allowed by the finite system memory).
So it's got nothing to do with the halting conjecture - we know this program will definitely halt, because we don't have infinite memory. It also doesn't solve the conjecture, because it will halt. This seems like circular reasoning.
If we had an infinite machine then we could write a program that could solve the conjecture, if we had infinite time to run it in (or it ran infinitely fast). Because we don't have any of those things, writing a program to solve the conjecture is impossible, regardless of our ability to determine if it halted or not.
If we had the ability to determine if that program halted, we would still need an infinite machine to run the program, which we don't, so the ability to determine whether the program halts or not is irrelevant. We can't create such a program (because we can trivially determine that any such program will actually halt - yes it does, because it runs out of memory).
One past discussion:
https://news.ycombinator.com/item?id=37204624 - 26 points by azhenley on Aug 21, 2023, 21 comments
Stephen Wolfram talks about computational irreducibility and I think of that as essentially the same as the halting problem. I like his description that science advances by finding problems that we care about that are also computationally reducible. An equivalent with halting is to find those problems that we care about where halting can be proven (or disproven).
[flagged]
This article is attacking a straw man.
The reason why the halting problem is of minor importance for pragmatically minded programmers has nothing to do with machine memory size. It's of minor importance because while it's intractably hard to prove an arbitrary program has some desired properties, it's considerably and practically easier to reliably construct a program with said properties. That problem of program construction is what we as programmers are trained and paid to do, and overall we do an adequate job of it.