8 ms·

What Computers Cannot Do: The Consequences of Turing-Completeness

71 points by gavinhoward 3y ago

Vecr 3y ago
There's no way this is an argument that humans can do things AIs can't do. Weird quantum nonsense won't help, because quantum computers aren't oracle machines.
- thethirdone 3y ago
  Its not. Mostly it is an argument that turing-completeness is too mathematical to be practical. > I still had the mainstream belief that AI would be just as capable as humans.
  - avmich 3y ago
    I'm not sure what is more mainstream - belief that AIs are as capable as humans, or belief that they are not. Roger Penrose is one of the more authoritative, for lack of other arguments, voices for humans being more capable than AIs. Still not sure if it implies an existence of God, a class of ability higher than Turing machine or something else.
    - forgotmyinfo 3y ago
      All it implies is that brains are immensely complicated and have kajillions of connections, which don't work the same as anything branded AI. Consciousness can be an emergent property AND AI capability can be largely oversold at the same time.
    - Vecr 3y ago
      > class of ability higher than Turing machine Yes it does, it would mean that your brain can somehow exploit quantum gravity to turn itself into an oracle machine. How a wet blob significantly hotter than room temperature (in the superconductor definition) is supposed to do that I don't know.
      - kian 3y ago
        that's a good question, but the electron transport chain and photosynthesis are both postulated/(known?) to exploit quantum effects at room temperature.
  - K0balt 3y ago
    Humans have not demonstrated any capability that is not theoretically computable, AFAIK.
    - _factor 3y ago
      I haven’t seen anything yet that a Turing machine can’t do that we do. A better question might be: Can we do things “faster” than a Turing machine theoretically can? If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage.
      - Vecr 3y ago
        > If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage. That's what I was getting at with the temp. comment, as I suppose an oracle machine could theoretically be classical.
- deleted 3y ago
  [deleted]
thethirdone 3y ago
Quite a comprehensive summary of the implications of Turing-Completeness. There aren't any outright errors that pop out to me which is high bar if other articles are anything to judge by. > This was “easy” because the other major thing about UTM’s is how well they generalize to proving that just about any property of an algorithm is not computable, in the general case. This paraphrasing of Rice's theorem is good enough, but the mathematical result is meaningless in the practical Turing Complete sense. Rice's theorem is misused often on the internet to put limits on static analysis, but in most cases you can successfully prove that a given program terminates. And by proving that, Rice's theorem no longer prevents you from proving anything. > That looks like an unprovable property, which is exactly what you would have in a Turing-complete language. > ... > In essence, your language is still Turing-complete in practice. The implication of this statement is that because it is not obvious how to prove a given statement, it must be impossible to prove ANY statements in the general case. No additional argument beyond Rice's theorem has been given to explain why proving other properties would be impossible in the general case. It is exactly this thought process that makes me strongly dislike Rice's theorem. It is easy to decide that "I must not be able to prove this because its impossible" even when it is practically provable.
kangalioo 3y ago
I don't believe only turing machines are capable of executing other turing machines... Surely lambda calculus can do the same? I was under the impression, lambda calculus can indeed execute itself with even less code than turing machines There's several very dubious claims that are stated way too confidently like this in the article, like "Yep, virus scanners are almost completely useless"
- gavinhoward 3y ago
  Author here. Yes, the lambda calculus can. They are equivalent. But Turing's machines gave us the model to think that way. In my opinion.
  - superjan 3y ago
    What does it for me is that turing machines can be thought of as physical. In a way it is more tangible than an electronic computer. Btw: I think your site would look better with left justified text. Right justified looks best only for long paragraphs (books).
    - gavinhoward 3y ago
      Yeah, I was told about left justification last week. Haven't gotten to it since I am in the middle of release crunch.
- forgotmyinfo 3y ago
  They are equivalent per the Church-Turing thesis; how many instructions it takes doesn't factor in at all.
kangalioo 3y ago
I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general
- AlotOfReading 3y ago
  It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain problems were outside that set.
  - kangalioo 3y ago
    Yeah, that's definitely fair. What I'm annoyed about is the "checkmate, computers" stance, pretending like the problems computers cannot solve could be solved by other means
  - haltIncomplete 3y ago
    It was obvious to Turing and Church because of Gödel; incompleteness theorem restated. Einstein, Gödel, and a few others verified work means the majority of us are coloring within the lines they drew until we die.
tromp 3y ago
> Because there is one aspect of Turing’s model that makes it more useful: Universal Turing Machines (UTM’s). > Universal Turing Machines The idea of UTM’s is that you can have Turing Machines running other Turing Machines. Just like you can have lambda terms running other lambda terms [1] [2]. In fact an additvely optimal [3] universal lambda term can be as simple as ┬─┬ ────────────────────────────────────────────────────┬─┬── ┬──────── └─┤ ────────────────────────────────────────────────────┼─┼─┬ │ ┬─┬ ┬─┬ │ ┬───────────────────────────────────────────────────┼─┼─┼ │ └─┤ ├─┘ │ │ ──┬────────────────────────────────────────────── ├─┘ │ │ ├─┘ │ │ ┬─┼─────────────────────────────────────────────┬ │ │ ├───┘ │ │ ┼─┼─┬─────────────┬───────────────────┬─────────┼ │ │ │ │ │ ┼─┼─┼───┬─────────┼─┬───────────┬─────┼─┬───────┼ │ │ │ │ │ │ ┼─┼─┬─┼─────────┼─┼─────────┬─┼───┬─┼─┼─────┬─┼ │ │ │ │ │ │ │ │ ┼─┼─┬───────┼─┼─┬────── │ │ ┬─┼ ┼─┼─────┼─┼ │ │ │ │ │ │ │ │ │ │ ┼─────┬ │ ┼─┼───┬── │ │ ├─┘ │ ┼─┬───┼ │ │ │ │ │ │ │ │ │ │ │ ┼───┬─┼ │ │ ┼─┬─┼─┬ │ ├─┘ │ │ ┼─┬─┼ │ │ │ │ │ │ │ │ │ │ │ │ ┬─┼─┼ │ │ └─┤ ├─┘ └─┤ │ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ │ └─┤ │ │ │ ├─┘ │ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ │ ├─┘ │ ├───┘ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ ├───┘ ├─┘ │ └─┤ │ │ │ │ │ │ │ │ │ │ ├─┘ │ │ ├───────┘ │ │ │ │ │ │ │ │ └─┤ │ ├───────┘ │ │ │ │ │ │ │ │ ├─────────┘ │ │ │ │ │ │ │ │ ├───┘ │ │ │ │ │ │ │ └─┤ │ │ │ │ │ │ │ ├───────────────────────────┘ │ │ │ │ │ ├───┘ │ │ │ │ └─┤ │ │ │ │ └─────────────────────────────────────────────────┤ │ │ │ ├───┘ │ └─────────────────────────────────────────────────────┤ │ └─────┘ in the graphical notation of [3], while an additively optimal TM would be monstrously complex. In that regard, Turing Machines are no more useful than the lambda calculus. [1] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861#lambda-encoding https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8... [2] https://rosettacode.org/wiki/Universal_Lambda_Machine https://rosettacode.org/wiki/Universal_Lambda_Machine [3] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861#universality https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8... [4] https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html
mateo1 3y ago
To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possible statements true or or false (or equivalent) within a formal system. For example you can't have a general program that you feed in any 2 mathematical statements and tells you if they're equal. From what I understand this is proven for "regular math" but not all formal systems. As a counterpoint, there are many algorithms these days that can do theorem proving better than anything before in history (partly thanks to AI, and partly thanks to the massive efforts that went into symbolic computation engines over the past decades). I think in a few years theorem proving will be done elegantly by computers instead of humans. Not all theorems, sure, but this is the world we got to live in.
- deleted 3y ago
  [deleted]
bionhoward 3y ago
(noob rant warning) What bugs me about the decidability thing, is Turing proved 2-undecidability in the action space {halt, loop}, but I still feel like we miss an opportunity to try 3-decidability {halt, loop, paradox} and throw out the functions upon which his proof hinged, namely, the ones that invoke the is_halting function and do the opposite. Also, the whole, "we make this other program that does the opposite" argument implies the test of `is_halting` is actually a test of some other function "do_opposite" that wraps "is_halting" and does the opposite. That's not exactly fair, that's a test of the opposite function, not the "is_halting" function. Furthermore, the inner "do_opposite" evaluated by is_halting, is a different invocation of the do_opposite source. (I.E. Fregeian Sense and Reference, a different referent for the same sense). Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. Furthermore, is_halting could theoretically refuse to play ball and crash the program at runtime, or induce a compile error before the game can even begin, if we try to create a paradox. Has anyone actually even witnessed a real paradox in real life? Maybe the universe is deeply anti-paradox and the whole argument is a bunch of humbug. Can someone please tell me how I'm fooling myself? Cuz I'm neck deep in coding this thing and building all the helper functions and it would save a bunch of time to know why it's wrong. Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? If the caller wants to do_opposite, that's their problem, not on is_opposite. A function which can decide halting for all the non_opposite functions (which is, every one that matters in practice, right?) Plus, who knows what an anti-paradox machine can accomplish? Maybe there's one weird trick quantum scientists or thermodynamic reversible computer engineers hate, and you can solve hard problems by finding the ones which both halt and don't. Just feels weird how we all accept this quasi-religious belief that we shouldn't even try to decide if programs halt simply because you can't categorize every single program into 2 buckets. What about 3 buckets i.e. 3-decidability of the ternary halting problem? sorry for long comment, fuck it, ill post code, it sucks and doesn't run, just tinkering, but https://github.com/bionicles/halts https://github.com/bionicles/halts published for your pleasure. No promise it will ever actually work.
- klyrs 3y ago
  Does the following terminate for all n? def foo(n): if n <= 1: return elif n & 1: return foo(3*n+1) else: return foo(n//2)
neallindsay 3y ago
"Some mother**ers are always trying to solve the halting problem."—Wesley Snipes, Blade
- deleted 3y ago
  [deleted]
iainmerrick 3y ago
I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thrown away? Strong static typing? It's generally possible to write valid programs (i.e., that would run successfully without runtime errors) that don't type-check successfully. So the set of type-safe programs is smaller than the set of useful programs. Is that an argument for discarding type safety? No, because the vast majority of programs we want to write can be type-checked and it's useful to do so. Termination checking? This post has a nice example of an effectively-non-terminating loop in Bazel. Bazel's control language doesn't have unbounded loops, so the author just nests a bunch of very long loops. It's fun, but "it's possible to write a Bazel build script that takes an infeasibly long time to run, effectively infinite" doesn't seem like a problem in practice. It's still hard to write such a thing accidentally!
- crq-yml 3y ago
  Hot take, it's an author who wants total power over computers and is upset that Turing completeness impedes that power. If they were thinking pragmatically they wouldn't have gotten into the argument linked in the post about Zig comptime.
  - gavinhoward 3y ago
    Author here. No, I do not.
s4mw1se 3y ago
I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core. The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a company that made a SAST product and I had to support the scanner for companies across the globe. There will always be a 0-day market because of Halting problem. If you think down the road 20 years. Virtually everything we touch will have internet. It will all depend on a program checking a program. Since no computer can guarantee its correctness on its own. Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. A book I read had a quote that said if you want to make a product that will generate infinite profit, create a static analysis scanner. I’m not a mathematician but the Halting problem always reminds me of the Godels incompleteness theorem in a way. I think these are the greatest gifts humanity has ever discovered. It means there is always hope for humanity as long as oppression depends on technology, because the technology will always be flawed. There is always a undiscovered theorem that has to potential to change everything we know.
- MikeBattaglia 3y ago
  > Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.
- poorlyknit 3y ago
  If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin. ISBN is 3423300175.
  - s4mw1se 3y ago
    Funny you recommended this book. It what inspired me to go back to school and enroll in compsci. I forgot that’s where this seed was planted. I think it’s safe to say it really resonated with me lol. I really appreciate your comment. That book has been sitting behind me on my bookshelf for years blending into background. I just pulled it off the shelf. I just graduated a few weeks ago after working on my BS for 10 years. The fact that you brought this book up, the piece that inspired me to go back to school in the first place… is something Hofstadter would probably refer as my minds I recursive loop of existence. Something of that sentiment at least
jhanschoo 3y ago
The author cites this https://news.ycombinator.com/item?id=35683634 https://news.ycombinator.com/item?id=35683634 as evidence that his interlocutor doesn't understand the halting problem. But the halting problem is a hard limit that is of concern only for computers with infinite memory. In practice we are unable to compile (and run) many perfectly valid programs due to RAM constraints, and some systems are able to compile programs that others cannot. People looking to compile useful programs already accept these inevitable limits, yet the author seems to think that some notion of fuel in compilation time makes a compiler terribly compromised. https://news.ycombinator.com/item?id=35707565 https://news.ycombinator.com/item?id=35707565
lifthrasiir 3y ago
Any sufficiently expressive type system is undecidable anyway (including Rust's), so it is futile to limit the practical Turing completeness as opposed to the theoretical Turing completeness.
mkleczek 3y ago
This subject requires mandatory link to the excellent and eye opening talk by Ron Pressler: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

71 points by gavinhoward 3y ago

Vecr 3y ago

There's no way this is an argument that humans can do things AIs can't do. Weird quantum nonsense won't help, because quantum computers aren't oracle machines.

thethirdone 3y ago
Its not. Mostly it is an argument that turing-completeness is too mathematical to be practical. > I still had the mainstream belief that AI would be just as capable as humans.
- avmich 3y ago
  I'm not sure what is more mainstream - belief that AIs are as capable as humans, or belief that they are not. Roger Penrose is one of the more authoritative, for lack of other arguments, voices for humans being more capable than AIs. Still not sure if it implies an existence of God, a class of ability higher than Turing machine or something else.
  - forgotmyinfo 3y ago
    All it implies is that brains are immensely complicated and have kajillions of connections, which don't work the same as anything branded AI. Consciousness can be an emergent property AND AI capability can be largely oversold at the same time.
  - Vecr 3y ago
    > class of ability higher than Turing machine Yes it does, it would mean that your brain can somehow exploit quantum gravity to turn itself into an oracle machine. How a wet blob significantly hotter than room temperature (in the superconductor definition) is supposed to do that I don't know.
    - kian 3y ago
      that's a good question, but the electron transport chain and photosynthesis are both postulated/(known?) to exploit quantum effects at room temperature.
- K0balt 3y ago
  Humans have not demonstrated any capability that is not theoretically computable, AFAIK.
  - _factor 3y ago
    I haven’t seen anything yet that a Turing machine can’t do that we do. A better question might be: Can we do things “faster” than a Turing machine theoretically can? If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage.
    - Vecr 3y ago
      > If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage. That's what I was getting at with the temp. comment, as I suppose an oracle machine could theoretically be classical.
deleted 3y ago
[deleted]

thethirdone 3y ago

Quite a comprehensive summary of the implications of Turing-Completeness. There aren't any outright errors that pop out to me which is high bar if other articles are anything to judge by. > This was “easy” because the other major thing about UTM’s is how well they generalize to proving that just about any property of an algorithm is not computable, in the general case. This paraphrasing of Rice's theorem is good enough, but the mathematical result is meaningless in the practical Turing Complete sense. Rice's theorem is misused often on the internet to put limits on static analysis, but in most cases you can successfully prove that a given program terminates. And by proving that, Rice's theorem no longer prevents you from proving anything. > That looks like an unprovable property, which is exactly what you would have in a Turing-complete language. > ... > In essence, your language is still Turing-complete in practice. The implication of this statement is that because it is not obvious how to prove a given statement, it must be impossible to prove ANY statements in the general case. No additional argument beyond Rice's theorem has been given to explain why proving other properties would be impossible in the general case. It is exactly this thought process that makes me strongly dislike Rice's theorem. It is easy to decide that "I must not be able to prove this because its impossible" even when it is practically provable.

kangalioo 3y ago

I don't believe only turing machines are capable of executing other turing machines... Surely lambda calculus can do the same? I was under the impression, lambda calculus can indeed execute itself with even less code than turing machines There's several very dubious claims that are stated way too confidently like this in the article, like "Yep, virus scanners are almost completely useless"

gavinhoward 3y ago
Author here. Yes, the lambda calculus can. They are equivalent. But Turing's machines gave us the model to think that way. In my opinion.
- superjan 3y ago
  What does it for me is that turing machines can be thought of as physical. In a way it is more tangible than an electronic computer. Btw: I think your site would look better with left justified text. Right justified looks best only for long paragraphs (books).
  - gavinhoward 3y ago
    Yeah, I was told about left justification last week. Haven't gotten to it since I am in the middle of release crunch.
forgotmyinfo 3y ago
They are equivalent per the Church-Turing thesis; how many instructions it takes doesn't factor in at all.

kangalioo 3y ago

I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general

AlotOfReading 3y ago
It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain problems were outside that set.
- kangalioo 3y ago
  Yeah, that's definitely fair. What I'm annoyed about is the "checkmate, computers" stance, pretending like the problems computers cannot solve could be solved by other means
- haltIncomplete 3y ago
  It was obvious to Turing and Church because of Gödel; incompleteness theorem restated. Einstein, Gödel, and a few others verified work means the majority of us are coloring within the lines they drew until we die.

tromp 3y ago

> Because there is one aspect of Turing’s model that makes it more useful: Universal Turing Machines (UTM’s). > Universal Turing Machines The idea of UTM’s is that you can have Turing Machines running other Turing Machines. Just like you can have lambda terms running other lambda terms [1] [2]. In fact an additvely optimal [3] universal lambda term can be as simple as ┬─┬ ────────────────────────────────────────────────────┬─┬── ┬──────── └─┤ ────────────────────────────────────────────────────┼─┼─┬ │ ┬─┬ ┬─┬ │ ┬───────────────────────────────────────────────────┼─┼─┼ │ └─┤ ├─┘ │ │ ──┬────────────────────────────────────────────── ├─┘ │ │ ├─┘ │ │ ┬─┼─────────────────────────────────────────────┬ │ │ ├───┘ │ │ ┼─┼─┬─────────────┬───────────────────┬─────────┼ │ │ │ │ │ ┼─┼─┼───┬─────────┼─┬───────────┬─────┼─┬───────┼ │ │ │ │ │ │ ┼─┼─┬─┼─────────┼─┼─────────┬─┼───┬─┼─┼─────┬─┼ │ │ │ │ │ │ │ │ ┼─┼─┬───────┼─┼─┬────── │ │ ┬─┼ ┼─┼─────┼─┼ │ │ │ │ │ │ │ │ │ │ ┼─────┬ │ ┼─┼───┬── │ │ ├─┘ │ ┼─┬───┼ │ │ │ │ │ │ │ │ │ │ │ ┼───┬─┼ │ │ ┼─┬─┼─┬ │ ├─┘ │ │ ┼─┬─┼ │ │ │ │ │ │ │ │ │ │ │ │ ┬─┼─┼ │ │ └─┤ ├─┘ └─┤ │ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ │ └─┤ │ │ │ ├─┘ │ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ │ ├─┘ │ ├───┘ │ │ ├─┘ │ │ │ │ │ │ │ │ │ │ │ ├───┘ ├─┘ │ └─┤ │ │ │ │ │ │ │ │ │ │ ├─┘ │ │ ├───────┘ │ │ │ │ │ │ │ │ └─┤ │ ├───────┘ │ │ │ │ │ │ │ │ ├─────────┘ │ │ │ │ │ │ │ │ ├───┘ │ │ │ │ │ │ │ └─┤ │ │ │ │ │ │ │ ├───────────────────────────┘ │ │ │ │ │ ├───┘ │ │ │ │ └─┤ │ │ │ │ └─────────────────────────────────────────────────┤ │ │ │ ├───┘ │ └─────────────────────────────────────────────────────┤ │ └─────┘ in the graphical notation of [3], while an additively optimal TM would be monstrously complex. In that regard, Turing Machines are no more useful than the lambda calculus. [1] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861#lambda-encoding https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8... [2] https://rosettacode.org/wiki/Universal_Lambda_Machine https://rosettacode.org/wiki/Universal_Lambda_Machine [3] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861#universality https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8... [4] https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html

mateo1 3y ago

To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possible statements true or or false (or equivalent) within a formal system. For example you can't have a general program that you feed in any 2 mathematical statements and tells you if they're equal. From what I understand this is proven for "regular math" but not all formal systems. As a counterpoint, there are many algorithms these days that can do theorem proving better than anything before in history (partly thanks to AI, and partly thanks to the massive efforts that went into symbolic computation engines over the past decades). I think in a few years theorem proving will be done elegantly by computers instead of humans. Not all theorems, sure, but this is the world we got to live in.

deleted 3y ago
[deleted]

bionhoward 3y ago

(noob rant warning) What bugs me about the decidability thing, is Turing proved 2-undecidability in the action space {halt, loop}, but I still feel like we miss an opportunity to try 3-decidability {halt, loop, paradox} and throw out the functions upon which his proof hinged, namely, the ones that invoke the is_halting function and do the opposite. Also, the whole, "we make this other program that does the opposite" argument implies the test of `is_halting` is actually a test of some other function "do_opposite" that wraps "is_halting" and does the opposite. That's not exactly fair, that's a test of the opposite function, not the "is_halting" function. Furthermore, the inner "do_opposite" evaluated by is_halting, is a different invocation of the do_opposite source. (I.E. Fregeian Sense and Reference, a different referent for the same sense). Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. Furthermore, is_halting could theoretically refuse to play ball and crash the program at runtime, or induce a compile error before the game can even begin, if we try to create a paradox. Has anyone actually even witnessed a real paradox in real life? Maybe the universe is deeply anti-paradox and the whole argument is a bunch of humbug. Can someone please tell me how I'm fooling myself? Cuz I'm neck deep in coding this thing and building all the helper functions and it would save a bunch of time to know why it's wrong. Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? If the caller wants to do_opposite, that's their problem, not on is_opposite. A function which can decide halting for all the non_opposite functions (which is, every one that matters in practice, right?) Plus, who knows what an anti-paradox machine can accomplish? Maybe there's one weird trick quantum scientists or thermodynamic reversible computer engineers hate, and you can solve hard problems by finding the ones which both halt and don't. Just feels weird how we all accept this quasi-religious belief that we shouldn't even try to decide if programs halt simply because you can't categorize every single program into 2 buckets. What about 3 buckets i.e. 3-decidability of the ternary halting problem? sorry for long comment, fuck it, ill post code, it sucks and doesn't run, just tinkering, but https://github.com/bionicles/halts https://github.com/bionicles/halts published for your pleasure. No promise it will ever actually work.

klyrs 3y ago
Does the following terminate for all n? def foo(n): if n <= 1: return elif n & 1: return foo(3*n+1) else: return foo(n//2)

neallindsay 3y ago

"Some mother**ers are always trying to solve the halting problem."—Wesley Snipes, Blade

deleted 3y ago
[deleted]

iainmerrick 3y ago

I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thrown away? Strong static typing? It's generally possible to write valid programs (i.e., that would run successfully without runtime errors) that don't type-check successfully. So the set of type-safe programs is smaller than the set of useful programs. Is that an argument for discarding type safety? No, because the vast majority of programs we want to write can be type-checked and it's useful to do so. Termination checking? This post has a nice example of an effectively-non-terminating loop in Bazel. Bazel's control language doesn't have unbounded loops, so the author just nests a bunch of very long loops. It's fun, but "it's possible to write a Bazel build script that takes an infeasibly long time to run, effectively infinite" doesn't seem like a problem in practice. It's still hard to write such a thing accidentally!

crq-yml 3y ago
Hot take, it's an author who wants total power over computers and is upset that Turing completeness impedes that power. If they were thinking pragmatically they wouldn't have gotten into the argument linked in the post about Zig comptime.
- gavinhoward 3y ago
  Author here. No, I do not.

s4mw1se 3y ago

I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core. The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a company that made a SAST product and I had to support the scanner for companies across the globe. There will always be a 0-day market because of Halting problem. If you think down the road 20 years. Virtually everything we touch will have internet. It will all depend on a program checking a program. Since no computer can guarantee its correctness on its own. Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. A book I read had a quote that said if you want to make a product that will generate infinite profit, create a static analysis scanner. I’m not a mathematician but the Halting problem always reminds me of the Godels incompleteness theorem in a way. I think these are the greatest gifts humanity has ever discovered. It means there is always hope for humanity as long as oppression depends on technology, because the technology will always be flawed. There is always a undiscovered theorem that has to potential to change everything we know.

MikeBattaglia 3y ago
> Exploits will always be able to chained, and everything will always be exploitable. Including AI systems. Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.
poorlyknit 3y ago
If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin. ISBN is 3423300175.
- s4mw1se 3y ago
  Funny you recommended this book. It what inspired me to go back to school and enroll in compsci. I forgot that’s where this seed was planted. I think it’s safe to say it really resonated with me lol. I really appreciate your comment. That book has been sitting behind me on my bookshelf for years blending into background. I just pulled it off the shelf. I just graduated a few weeks ago after working on my BS for 10 years. The fact that you brought this book up, the piece that inspired me to go back to school in the first place… is something Hofstadter would probably refer as my minds I recursive loop of existence. Something of that sentiment at least

jhanschoo 3y ago

The author cites this https://news.ycombinator.com/item?id=35683634 https://news.ycombinator.com/item?id=35683634 as evidence that his interlocutor doesn't understand the halting problem. But the halting problem is a hard limit that is of concern only for computers with infinite memory. In practice we are unable to compile (and run) many perfectly valid programs due to RAM constraints, and some systems are able to compile programs that others cannot. People looking to compile useful programs already accept these inevitable limits, yet the author seems to think that some notion of fuel in compilation time makes a compiler terribly compromised. https://news.ycombinator.com/item?id=35707565 https://news.ycombinator.com/item?id=35707565

lifthrasiir 3y ago

Any sufficiently expressive type system is undecidable anyway (including Rust's), so it is futile to limit the practical Turing completeness as opposed to the theoretical Turing completeness.

mkleczek 3y ago

This subject requires mandatory link to the excellent and eye opening talk by Ron Pressler: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity