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.
What Computers Cannot Do: The Consequences of Turing-Completeness
41–50 of 61 posts
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#42This subject requires mandatory link to the excellent and eye opening talk by Ron Pressler:
https://pron.github.io/posts/correctness-and-complexity
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#43I 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 com…
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
1. Unfortunately the set of "some" programs is unknown and most probably really small.
2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation.
3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#44> 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 ┬─┬ ─────────────────────────────────────────────…
I'm confused by your 'additively optimal' definition. Suppose that the objects we want to describe are strings of bits, and the description method D is just "listing the bits out in a sequence". Then surely no BLC term can describe the same sequence of bits with only a constant amount of overhead.
Then D is just identity, or λ 1, using only 4 bits of overhead?!
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#45(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"…
Does the following terminate for all n? def foo(n): if n
Running it for larger and larger numbers, will report back soon...
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#46(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"…
It is not clear to me what you would define as the reason to return paradox from `halts`. It is pretty clear you can make a `halts` function that returns halts, loop or unsure. Renaming unsure to paradox would give a valid version of your 3-decidable `halts`. A concrete definition in terms of turing machines is necessary if you want to displace the halting problem. > (I.E. Fregeian Sense and Reference, a different re…
Thank you for the reply! I certainly don't intend to put forward a claim that 3-decidability, if possible, would invalidate the 2-undecidability result; Rather, I believe it worth investigation to see if we allow ourselves a middle road of a paradox category, it's a different theorem and might be provable or at least practically useful.
Would "halts" be useless if it only decided every function except the ones that invoke it and do the opposite? If not, maybe it's worth building, even if we know it's not possible to classify everything into 2 buckets, because the majority of real world functions don't have that opposite property and could be useful to decide halting for that subset.
Also, I'd point out, there is a difference between the inner and outer invocations of the same turing machine. They are different executions of the same machine, on different layers. A decision about an inner machine might be truly correct, independent of whatever happens outside.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#47(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"…
The more tractable problem is {halt, loop, unknown}. That problem us trivially solvable, and solved by every static analysis tool and optimizing compiler. Or at least, the generalized {yes, no, maybe} problem for various properties is. The real question is, how small can you make the set of instances that results in "maybe", and how small can you make the intersection of that set, and the set of instances we actually…
I would define paradox specifically as the case involved in the proof of the 2-undecidability halting problem, namely, functions of this kind:
def do_opposite(): if is_halting(do_opposite): loop_forever()
That's the paradox function which allegedly proves it's not worth attempting to decide {halt, loop} and so that (and other functions with the same behavior) would belong in the paradox category.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#48(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"…
Does the following terminate for all n? def foo(n): if n
Collatz is not "theoretically undecidable" because of a paradox, it's "practically undecidable" because it has an infinite domain, so "is_halting" implemented via simulation would take infinite time to try every number.
Would you give an engineer an infinitely large project, criticize them for being unable to complete it, and use their 'failure' to support cancellation of a finite, smaller project with potential benefit?
Seems like just another lame argument to me.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#49Earlier quoted context omitted.
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
1. Unfortunately the set of "some" programs is unknown and most probably really small. 2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation. 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs. See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel.
> 1. Unfortunately the set of "some" programs is unknown and most probably really small.
Many useful algorithms can be proven to terminate. Compare against the situation in mathematics: many theorems are not be provable, but that does not stop us from trying to prove useful theorems, or recognizing that a given theorem has already been proven.
> 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
This is true in the sense that a proof of arbitrary program A does not tell us anything about many other programs. But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates.
Even the link you provide gives optimism and claims that
> Now we know why writing correct programs is hard: because it has to be. But while we cannot verify all programs all the time – regardless of how they’re written – there’s nothing stopping us from verifying some programs some of the time for some properties.
Re: What Computers Cannot Do: The Consequences of Turing-Completeness
#50Earlier quoted context omitted.
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs. This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
1. Unfortunately the set of "some" programs is unknown and most probably really small. 2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation. 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs. See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
> Proofs are not reuable: proving something about one program does not tell us anything about other programs.
They are reusable to some degree when the proofs are made with type systems, via Curry-Howard.