3 ms·

Yes, even people who are aware of the halting problem often misunderstand its implications. What Turing proved is that no algorithm -- in the sense of an effec

Yes, even people who are aware of the halting problem often misunderstand its implications. What Turing proved is that no algorithm -- in the sense of an effective procedure, that is guaranteed to return the correct answer in finite time on any input -- can solve the halting problem. But there is a critical difference between algorithms and heuristics. A heuristic is not guaranteed to do anything, but nonetheless, collections of heuristics can be assembled that can analyze properties of programs in many cases of actual interest. The distinction between algorithms and heuristics is, in my opinion, insufficiently appreciated. For example, the very phrase "genetic algorithms" is a contradiction in terms -- these are clearly heuristics, not algorithms. Anyway, back to your point, we who are still selling static analysis -- I'm not sure why you used the past tense there; it's a growing business -- find that people who don't understand the halting problem at all are perhaps as much a source of difficulty as those who are aware of it but don't understand its implications. The latter group are skeptical that our products can work at all, but the former are often baffled and indignant that the products don't understand properties of their code that seem obvious. (The fact that analysis often takes a long time and needs large amounts of RAM also surprises some people.) But I think the world is gradually coming to understand what static analysis can and can't do. It's an education process and will take time.

tedunangst 14y ago
Past tense because I no longer sell static analysis software.
- jdp23 14y ago
  Do you miss it? I sometimes do ...
scott_s 14y ago
The kinds of static analysis you're talking about are different than what Matt is talking about in his article. Matt is talking about situations where you can make guarantees. That is, if his analyzer says that a register can never take on a negative value, that is a guarantee. It is not based on a heuristic, it is based on a proof. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. If I understand you correctly, you're talking about heuristics which allow one to say "It is very likely that this program will exhibit that behavior." It's not a guarantee, because it's not based on a proof, but rather on heuristics which try to match patterns in the code in question to patterns in code that was known to exhibit such behavior. Carmack talks about using such static analysis in his projects in a popular blog post (HN discussions: http://news.ycombinator.com/item?id=4543553 http://news.ycombinator.com/item?id=4543553 and http://news.ycombinator.com/item?id=3388290 http://news.ycombinator.com/item?id=3388290). In simpler terms, Matt's approach avoids the halting problem by only providing guarantees on a limited set of behaviors. The approach you're talking about avoids the halting problem by not providing guarantees, but by providing likelihoods.
- ced 14y ago
  I agree with your post, though I am curious to know if there is any use for "this function is likely to terminate" inside static analysis. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. I would rather say: the halting problem shows that there exists at least one program for which it is impossible to prove termination - not that every termination problem is undecidable, as the trivial example "return 5;" shows.
  - kd0amg 14y ago
    I am curious to know if there is any use for "this function is likely to terminate" inside static analysis. Well, something like "this condition is likely to be true" could help give an estimate for whether a loop will run many times, which leads to things like a better estimate for the cost of spilling to the stack values used in that loop instead of keeping them in registers. the halting problem shows that there exists at least one program for which it is impossible to prove termination I'm not sure that "every halting checker has some input where it gives the wrong answer" permits the conclusion "there is some input where they all give the wrong answer." Is "the machine must generate a proof of its answer" what lets you make that extra leap?
  - scott_s 14y ago
    The conclusion "this function is likely to terminate" may not be helpful, but "this function is likely to leak memory" may be extraordinarily helpful. The reason that everyone brings up the halting problem in this context is not that we want to test programs if they halt. (Well, we may, but we're generally looking for other behaviors.) It's because for some behaviors, if you want to be able to handle all cases, then that problem can be reduced to the halting problem. Matt provides an excellent demonstration of this with array indices. I'm confused by your restatement, because it does not restate what I said. You're talking about the halting problem. I'm talking about proving general behaviors in programs, despite the theoretical result that solving the halting problem is impossible, and that many behaviors can be reduced to the halting problem. The solution, as Matt explains, is to find ways to describe behaviors so they do not reduce to the halting problem. Using this technique, you still can have false negatives ("I don't know"), but you can guarantee no false positives.

tedunangst 14y ago

Past tense because I no longer sell static analysis software.

jdp23 14y ago
Do you miss it? I sometimes do ...

scott_s 14y ago

The kinds of static analysis you're talking about are different than what Matt is talking about in his article. Matt is talking about situations where you can make guarantees. That is, if his analyzer says that a register can never take on a negative value, that is a guarantee. It is not based on a heuristic, it is based on a proof. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. If I understand you correctly, you're talking about heuristics which allow one to say "It is very likely that this program will exhibit that behavior." It's not a guarantee, because it's not based on a proof, but rather on heuristics which try to match patterns in the code in question to patterns in code that was known to exhibit such behavior. Carmack talks about using such static analysis in his projects in a popular blog post (HN discussions: http://news.ycombinator.com/item?id=4543553 http://news.ycombinator.com/item?id=4543553 and http://news.ycombinator.com/item?id=3388290 http://news.ycombinator.com/item?id=3388290). In simpler terms, Matt's approach avoids the halting problem by only providing guarantees on a limited set of behaviors. The approach you're talking about avoids the halting problem by not providing guarantees, but by providing likelihoods.

ced 14y ago
I agree with your post, though I am curious to know if there is any use for "this function is likely to terminate" inside static analysis. How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program. I would rather say: the halting problem shows that there exists at least one program for which it is impossible to prove termination - not that every termination problem is undecidable, as the trivial example "return 5;" shows.
- kd0amg 14y ago
  I am curious to know if there is any use for "this function is likely to terminate" inside static analysis. Well, something like "this condition is likely to be true" could help give an estimate for whether a loop will run many times, which leads to things like a better estimate for the cost of spilling to the stack values used in that loop instead of keeping them in registers. the halting problem shows that there exists at least one program for which it is impossible to prove termination I'm not sure that "every halting checker has some input where it gives the wrong answer" permits the conclusion "there is some input where they all give the wrong answer." Is "the machine must generate a proof of its answer" what lets you make that extra leap?
- scott_s 14y ago
  The conclusion "this function is likely to terminate" may not be helpful, but "this function is likely to leak memory" may be extraordinarily helpful. The reason that everyone brings up the halting problem in this context is not that we want to test programs if they halt. (Well, we may, but we're generally looking for other behaviors.) It's because for some behaviors, if you want to be able to handle all cases, then that problem can be reduced to the halting problem. Matt provides an excellent demonstration of this with array indices. I'm confused by your restatement, because it does not restate what I said. You're talking about the halting problem. I'm talking about proving general behaviors in programs, despite the theoretical result that solving the halting problem is impossible, and that many behaviors can be reduced to the halting problem. The solution, as Matt explains, is to find ways to describe behaviors so they do not reduce to the halting problem. Using this technique, you still can have false negatives ("I don't know"), but you can guarantee no false positives.