Hacker News new | past | comments | ask | show | jobs | submit login

That's like saying that the undecidability of the halting problem has no practical effect because real world computers are actually finite state machines and not turing machines. This argument is true in only the most superficial way.

I haven't read the paper and so don't know how applicable it is, I just don't like your argument.

C++ grammar is undecidable [0]. The solution? Throwing your hands up and giving up on writing C++ compilers is certainly not the solution. Compiler writers just limit template instantiation depth making the compiler reject some correct programs.

[0]: http://blog.reverberate.org/2013/08/parsing-c-is-literally-u...

The undecidability of the halting problem has no practical effect.

That statement is too strong.

The practical effect is that you should not try to build an algorithm to detect infinite loops in general (though you wouldn't need undecidability for this, per se. E.g., NP-completeness of the halting problem would probably have been sufficient to kill attempts at a general algorithm dead in the water).

Of course, it is true in specific cases that you can decide whether a given program halts, and, indeed in almost all practical instances if you know how to solve a given problem then you should be able to construct an algorithm to solve it which provably halts. (Not including, of course, things that depend on environmental inputs, something that computes whether a given number satisfies Goldbach's conjecture, etc.)

There is, of course, enormous theoretical value in the undecidability of the halting problem, and in Kurt Gödel's undecidability of a general axiomatic system. And this theoretical value guides future theoretical research which is likely to lead to further practical value in future - which indicates a practical effect in the long-term. Also, of course, it indicates that an attempt to build a general theorem-prover is a useless endeavor (though approximate / specialized theorem provers are, of course, possible and indeed exist).

In particular, Gödel's undecidability has quite real implications for an Artificial General Intelligence which would have to reason about mathematics in general, and about its own thought processes in particular. Under classical mathematical reasoning, such an AI would be unable to "have confidence" in its own reasoning process. However, if the assumptions are relaxed from statements with 0/1 truth values to statements with probabilities, and time-independence of truth is relaxed, it is possible to define an agent which is able to assign (almost) consistent (actually "coherent") probabilities to what its own beliefs w̶i̶l̶l̶ ̶b̶e̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶m̶i̶t̶ ̶(̶a̶s̶ ̶t̶ ̶g̶o̶e̶s̶ ̶t̶o̶ ̶i̶n̶f̶i̶n̶i̶t̶y̶)̶) are at time t. See https://arxiv.org/abs/1609.03543 for more details. This is probably the strongest such statement that can be made in this class of arguments.

To be more concise. The undecidability of the halting problem has no practical effect, barring usual considerations about fundamental research.

Isn't it one of the reason limiting the power of static analysis and force us to use dynamic analysis to get certain information about the correctness of our programs ?

If the halting problem was merely NP complex, it would have still limited practical possibilities of static analysis.

Eh, modern SMT solvers are very practical tools, as are solvers for Mixed Integer Linear Programs. NP-completeness doesn't mean that you can't solve most instances you care about in reasonable time.

Yes. And the halting problem doesn't preclude static program analysis even if it works with only a subset of all possible programs.

It looks like we're in perfect agreement then.

Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact