4 ms·

Actually building such a computer is provably impossible: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem I highl

Actually building such a computer is provably impossible: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem I highly recommend this talk on the subject: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

legalcorrection 4y ago
Rice’s theorem says no such thing. Rice’s theorem tells you you can’t necessarily prove you’ve built a flawless system, not that you can’t build a flawless system. You can build a perfect program even if you can’t necessarily then know you have. Perhaps you interpreted my post to suggest that you could build a machine that verifies that any arbitrary software run on it never enters an invalid state? If so, I agree, that is not possible. I made a minor edit to make it clear what I’m talking about.
- mkleczek 4y ago
  > Rice’s theorem tells you you can’t prove you’ve built a flawless system, not that you can’t build a flawless system. If you think about it - it is the same: how do you know the system you just built is flawless?
  - ncmncm 4y ago
    Because you built it in a series of steps, exactly zero of which introduced any undecidability.
    - mkleczek 4y ago
      See above - there is no reliable procedure (algorithm) that would allow you to build a TM with arbitrary properties (ie. implementing arbitrary requirements).
      - SAI_Peregrinus 4y ago
        Programs don't have to have Turing-complete behavior. Compilers do, but not every program needs to implement uncomputable behavior on its inputs.
        mkleczek 4y ago
        Actually it's the other way around: In reality most interesting programs accept Turing complete languages - albeit not formally specified :)
  - legalcorrection 4y ago
    You don't, but it's still flawless. My point was that it was theoretically, not practically possible. So your retort that it's not practically possible is kind of missing the point.
    - mkleczek 4y ago
      My point is that it is _theoretically_ not possible: there is no algorithm that would allow you to build a TM implementing arbitrary requirements. You have to use ad-hoc methods but then it is not possible to know your ad-hoc method is correct! So by "flawless" you can only mean "having some property but we cannot say what property it is". Edit: added "flawless" definition
      - legalcorrection 4y ago
        I'm not sure you're getting this. Let's say you want to build a video chat application with all of the same features as Zoom and not a single bug. That is, in fact, possible. Nothing about Rice's Theorem says you can't build a program without bugs. You can build a flawless video chat application. You won't, but you can. How? Very easy. Every time you're about to write code with a bug, don't. Write that same code but without the bug.
        mkleczek 4y ago
        > Every time you're about to write code with a bug, don't. Write that same code but without the bug. This procedure (algorithm) is ill-defined (is not realisable by a TM) as it would require verifying two things: a) the code you are about to write has a bug (ie. has a specific property) b) the code you wrote does not have a bug (ie. has a specific property) Rice's theorem says both are impossible.
        legalcorrection 4y ago
        Maybe moving to a specific instance of Rice's theorem is clearer. My point is that while he can't solve the halting problem—i.e. he can't reliably determine whether any arbitrary program will halt—an infallible programmer can reliably write his own programs such that they always halt. So, to go back to the original point, you can't reliably determine the correctness of every possible program. But you could, if you were not prone to error like all humans, always write your own programs such that they are always correct.
librexpr 4y ago
Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs where we can prove their correctness / incorrectness. What's more, I'd argue that if you're writing code whose behaviour is literally undecidable, you're doing something wrong, unless you're doing it for research purposes or something like that.
- mkleczek 4y ago
  > Rice's Theorem isn't as strong as you say it is It is very strong: its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties (if there was such an algorithm we could use it to build a TM that solves the halting problem) So for any non-trivial property the only way to build a TM with this property is to use some ad-hoc method (as there is no general algorithm) - but how do we know the TM we've just built really holds the property we wanted it to? There is no way to verify it due to Rice's theorem.
  - feanaro 4y ago
    This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.
    - mkleczek 4y ago
      There are two problems with this: 1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help. 2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.
      - ncmncm 4y ago
        It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.

legalcorrection 4y ago

Rice’s theorem says no such thing. Rice’s theorem tells you you can’t necessarily prove you’ve built a flawless system, not that you can’t build a flawless system. You can build a perfect program even if you can’t necessarily then know you have. Perhaps you interpreted my post to suggest that you could build a machine that verifies that any arbitrary software run on it never enters an invalid state? If so, I agree, that is not possible. I made a minor edit to make it clear what I’m talking about.

mkleczek 4y ago
> Rice’s theorem tells you you can’t prove you’ve built a flawless system, not that you can’t build a flawless system. If you think about it - it is the same: how do you know the system you just built is flawless?
- ncmncm 4y ago
  Because you built it in a series of steps, exactly zero of which introduced any undecidability.
  - mkleczek 4y ago
    See above - there is no reliable procedure (algorithm) that would allow you to build a TM with arbitrary properties (ie. implementing arbitrary requirements).
    - SAI_Peregrinus 4y ago
      Programs don't have to have Turing-complete behavior. Compilers do, but not every program needs to implement uncomputable behavior on its inputs.
      - mkleczek 4y ago
        Actually it's the other way around: In reality most interesting programs accept Turing complete languages - albeit not formally specified :)
- legalcorrection 4y ago
  You don't, but it's still flawless. My point was that it was theoretically, not practically possible. So your retort that it's not practically possible is kind of missing the point.
  - mkleczek 4y ago
    My point is that it is _theoretically_ not possible: there is no algorithm that would allow you to build a TM implementing arbitrary requirements. You have to use ad-hoc methods but then it is not possible to know your ad-hoc method is correct! So by "flawless" you can only mean "having some property but we cannot say what property it is". Edit: added "flawless" definition
    - legalcorrection 4y ago
      I'm not sure you're getting this. Let's say you want to build a video chat application with all of the same features as Zoom and not a single bug. That is, in fact, possible. Nothing about Rice's Theorem says you can't build a program without bugs. You can build a flawless video chat application. You won't, but you can. How? Very easy. Every time you're about to write code with a bug, don't. Write that same code but without the bug.
      - mkleczek 4y ago
        > Every time you're about to write code with a bug, don't. Write that same code but without the bug. This procedure (algorithm) is ill-defined (is not realisable by a TM) as it would require verifying two things: a) the code you are about to write has a bug (ie. has a specific property) b) the code you wrote does not have a bug (ie. has a specific property) Rice's theorem says both are impossible.
        legalcorrection 4y ago
        Maybe moving to a specific instance of Rice's theorem is clearer. My point is that while he can't solve the halting problem—i.e. he can't reliably determine whether any arbitrary program will halt—an infallible programmer can reliably write his own programs such that they always halt. So, to go back to the original point, you can't reliably determine the correctness of every possible program. But you could, if you were not prone to error like all humans, always write your own programs such that they are always correct.

librexpr 4y ago

Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs where we can prove their correctness / incorrectness. What's more, I'd argue that if you're writing code whose behaviour is literally undecidable, you're doing something wrong, unless you're doing it for research purposes or something like that.

mkleczek 4y ago
> Rice's Theorem isn't as strong as you say it is It is very strong: its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties (if there was such an algorithm we could use it to build a TM that solves the halting problem) So for any non-trivial property the only way to build a TM with this property is to use some ad-hoc method (as there is no general algorithm) - but how do we know the TM we've just built really holds the property we wanted it to? There is no way to verify it due to Rice's theorem.
- feanaro 4y ago
  This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.
  - mkleczek 4y ago
    There are two problems with this: 1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help. 2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.
    - ncmncm 4y ago
      It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.