Comment by nostrademons | Hacker News Reader

Comment by nostrademons | Hacker News Reader

Parent Full thread

The halting problem is often misunderstand as "computers can never detect if a program halts". It actually states that "computers can never detect if an arbitrary program halts".

There is a fairly large subset of useful programs that can be proven to halt. Anything that uses straight-line linear control flow. So can anything with that plus conditionals. So can that plus foreach loops, as long as iterators do not reflect updates to their underlying collections. Add a "forever { ... }" construct and you can prove that the program will not halt; in combination with the other constructs, you can prove liveness on each request handler while also guaranteeing that the server itself will never go down.

The two constructs you have to watch out for are loops that mutate state used in the conditional and unbounded recursion. Even for these, there are techniques to increase the set of programs that can be reasoned about, eg. using dataflow analysis to identify which state is mutable and preventing it from being used in conditionals or tracking data & codata through the typesystem.

http://blog.sigfpe.com/2007/07/data-and-codata.html

Such a language would not be Turing-complete; you won't be able to write an interpreter for a Turing-complete programming language in it. But the majority of common business problems don't require an interpreter for another programming language; most of them focus on storing data, triggering events, or computing functions of data.

I commented in a similar vein on a piece that said that smart contract environments should never use Turing-complete languages because of the undecidability of program properties: https://news.ycombinator.com/item?id=11942015 (That piece seemed to have a misconception that you can never prove properties of programs, rather than that you can't always prove properties of programs.)

The halting problem also makes an assumption on the program's size. In practice we probably only care about programs under, say, a billion petabytes (or any other finite limit you can think of). In theory you can have a Turing machine that solves this regardless of the program's structure.

If you mean "programs that can only use a billion petabytes of storage", then that's true, but if you mean "programs whose code is less than a billion petabytes long", it's not true. (Someone recently calculated a result that I think can be interpreted directly as an actual decidability bound, and it's dramatically shorter than that.)

I meant that there exists a TM which solves HP for programs smaller than a given size. This makes it computable. Now, just because we can prove the existence of a TM, doesn't mean we can find it. It's true that for programs which use a finite amount of storage we can actually describe the algorithm for the TM, but that's not what I meant.

This seems to be a weird issue conceptually:

http://mathoverflow.net/a/153106

Because of the list of correct answers for a finite subset of the Halting Problem is finite, the Turing machine you mention does exist, but we not only can't find it, we can't know when we've found it!

Where the Math Overflow post mentions that "experts could compute the particular value of n", there has recently been such a bound published in a thesis, such that we can be confident that we can never construct or recognize the solutions beyond that point (using a particular axiomatization of mathematics).

You referred to the idea that "you can have a Turing machine that solves this", and we can agree on that with the caveat that, above certain problem instance sizes, you can't know or verify in any way that you have such a Turing machine!

Yes, this is absolutely correct. If you give up on Turing-completeness you can prove that a subset of programs halt. A computer could search this infinite space for programs that solve a particular problem. However, there may not be a program P in this space that solves the problem in question so the problem of finding P in the subset of provably haltable programs does not necessarily halt.

My argument stands. Unless the halting problem is overcome, there will still be jobs for humans to write Turing-complete programs.

You merely defined halting problem. You did not argue the following:

Turing machine X can produce programs that meets certain specifications => Turing machine X solves the halting problem.

I'm not trying to make that argument.

Reply on news.ycombinator.com