Hacker News Reader

Comment by comex | Hacker News Reader

Although anyone worth their salt should recognize the halting problem, I'll point out that the vast majority of programs can be proven to terminate or not, and although testing for halting in particular isn't especially useful for real-life programs, it could be used as a benchmark for a more general theorem-proving tool of the sort that would be very useful for avoiding bugs.

Of course, a tool that could automatically prove useful properties about programs with no guidance, which would be significantly superior than all existing practical program analysis tools which require quite a lot of guidance, might be beyond the capabilities of the people that post bids for $300. Unless it used Mechanical Turk. :)

View on HN

There exist research programming languages that support 'total functions', that can be proven to always halt. Usually you divide the world into functions and cofunctions, and data and codata, the latter of which may be infinite (such as I/O).

I wish this were a more popular thing. When I write a function, I can probably enumerate in my head all the things I want it to do, and not halting usually isn't one of those things. But the instinctive reaction is to worry about Turing-completeness, which is puzzling. When's the last time you wanted a program with fundementally unprovable behavior?

Programming with such functions is called total functional programming. Here's a nice little introduction to the subject[1], and if you're a fan of code and math you should probably check out the other blog entries as well.

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

When's the last time you wanted a program with fundementally unprovable behavior?

I'm working on one today. I'm analyzing a data set for tens of millions of possible statistical anomalies, and I'm putting my "investigate further" threshold to statistically one in billions. Each thing added increases the size of the search space.

Knowing that it is extremely unlikely to run forever really is good enough. Proving that it won't is a non-issue for me. (Right now it takes several hours to run.)

> When I write a function, I can probably enumerate in my head all the things I want it to do, and not halting usually isn't one of those things. But the instinctive reaction is to worry about Turing-completeness, which is puzzling. When's the last time you wanted a program with fundementally unprovable behavior?

You don't usually want fundamentally unprovable behavior. However, you also don't want to sacrifice the ability to compute anything that is computable. And you can't throw out the bathwater of the halting problem without throwing out the baby of computing everything computable.

So, in practice, you want to use provably-halting-on-all-valid-inputs algorithms for the problems where you have available (either known, or that you can find with reasonable effort) such an algorithm, but retain the option of using other techniques for other problems.

AI?

> Although anyone worth their salt should recognize the halting problem

Bah humbug. You can be a totally competent engineer and not immediately recognise the halting problem, just like you can be a totally competent auto-mechanical engineer and not recognise a oxidation-reduction reaction.

You can solve high-value real business problems every day for the rest of your life and never encounter a single decision that will be meaningfully informed by knowing about the halting problem.

Computer science != software engineering.

> You can solve high-value real business problems every day for the rest of your life and never encounter a single decision that will be meaningfully informed by knowing about the halting problem.

I dunno; I find that plenty of times dealing with fairly pedestrian business-problem requests its not uncommon to run into something that is desired that is equivalent to solving the halting problem; recognizing the difference between problems that are merely difficult and potentially expensive and risky investments of time and ones that are knowably impossible is pretty useful in terms of choosing where to allocate time and effort.

> Computer science != software engineering.

True, but software engineering depends on computer science, and, as in any form of engineering, understanding the well-known outer theoretical limits of what can be done is pretty important to engineering.

A good software engineer will know that there are limits to his capabilities, so my point is that in practice it's useless to differentiate between "merely difficult and potentially expensive and risky investments of time" and "knowably impossible", because, with the resources at hand, the former will, in fact, be impossible.

> True, but software engineering depends on computer science, and, as in any form of engineering, understanding the well-known outer theoretical limits of what can be done is pretty important to engineering.

I disagree - you can get by very well by understanding the inner, practical limits. Again, just like an auto-mechanical engineer: He doesn't need to understand the details of combustion or the process of refining oil, just enough to understand it works in the context of his domain: engineering cars. On the other hand, he also needs to know a little about suspension (but not the calculus of the harmonic oscillator) and enough metallurgy to weld the chassis safely.

And don't get me started on computer scientists that can't code.

> A good software engineer will know that there are limits to his capabilities, so my point is that in practice it's useless to differentiate between "merely difficult and potentially expensive and risky investments of time" and "knowably impossible", because, with the resources at hand, the former will, in fact, be impossible.

In practice, many of the most useful things to invest time and energy in are difficult, potentially expensive, and risky (often, because of the risk, you want to dual track this with a less-risky, lower-payoff approach) things that have high payoffs if successful.

OTOH, the knowably impossible things are dead ends. So, no, they aren't the same thing in practice.

Reply on news.ycombinator.com