← Back to context

Comment by nostrademons

10 years ago

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.

9 comments

nostrademons

Reply
schoen  10 years ago

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.)

liadmat  10 years ago

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.

  • schoen  10 years ago

    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.)

    • liadmat  10 years ago

      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.

      1 reply →

jcoffland  10 years ago

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.