4 ms·

I kinda hate that people dress up this analysis as a theorem. We have lots of formally verified programs that show useful work can be done here. And even if w

I kinda hate that people dress up this analysis as a theorem. We have lots of formally verified programs that show useful work can be done here. And even if we can't prove most of it, high assurance methods are very useful for preventing fuckery. I can't mathematically prove any lock is unpickable. But I can use a lock advanced enough that the cost of picking it becomes absurd. Also, theoretical quantum computers can solve whether a problem halts 100% of the time. So Rice's Theorem is theoretically meaningless.

tsimionescu 2y ago
> We have lots of formally verified programs that show useful work can be done here. Yes, by restricting things to a non-Turing Complete subset. > Also, theoretical quantum computers can solve whether a problem halts 100% of the time. That is absolutely not true. Quantum computers are proven to be entirely equivalent to classical computers in terms of what problems they can solve. The only difference is that they seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.
- lou1306 2y ago
  > Yes, by restricting things to a non-Turing Complete subset. No, not necessarily. There are procedures that _can_ verify properties against Turing-complete and even infinite-state systems. It's just that no _general_ (as in, sound and complete) procedure can exist.
  - tsimionescu 2y ago
    If it's not sound, than the result is meaningless. If it is not complete, then it only works on a subset of problems, which is equivalent to what I said.
    - lou1306 2y ago
      Agree that soundness is desirable, but "it only works on a subset of instances" and "you are restricted to a non-Turing complete subset" are not equivalent in the slightest.
      - deleted 2y ago
        [deleted]
      - lostmsu 2y ago
        Not sure what are you trying to say. Surely the "subset of instances" is non-Turing complete.
- isaacfrond 2y ago
  huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one? <citation missing>
  - tsimionescu 2y ago
    I'm not sure what you're asking about. It is well known that certain computations can be determinstically proven to halt - there's even a prigramming language that only accepts programs that do so, Idris. Of course, not any computation can be written in such a way. But it's clearly possible to write certain programs in such a way that they must halt by construction. You can even do it in C: don't use goto, only use loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i < 100; i++) is ok, as long as i is not modified in the body), don't use in-line ASM, don't use recursion, don't use stdlib functions (definitely no string functions). These rules can be verified syntactically (+- problems with UB), and the resulting program is guaranteed to halt. But there are problems for which you can't write such a program. As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.
    - Tainnor 2y ago
      > there's even a prigramming language that only accepts programs that do so, Idris. If you declare every function total. Idris still allows partial functions, and you can even cheat the whole system with "assert_total". Of course, with some sort of linter, you could still make sure that everything is actually total (although technically, in Idris "total" doesn't necessarily mean "halts" - programs which generate infinite input are also total in Idris).
frabert 2y ago
> We have lots of formally verified programs that show useful work can be done here Yes, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.
darby_nine 2y ago
Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm. Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages. Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time. If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are. It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.
- bionhoward 2y ago
  Relevant video about MIP*=RE https://youtu.be/2H8629BCbkM https://youtu.be/2H8629BCbkM
  - ykonstant 2y ago
    Lovely video!
- arethuza 2y ago
  Also worth noting that, from a practical perspective, even very simple programs/TMs can exhibit very complex behaviours that make it difficult to work out whether they will actually halt or not. At the time of writing there are 2833 5 state binary TMs that haven't been decided yet: https://github.com/bbchallenge/bbchallenge-undecided-index/blob/main/bb5_undecided_machines.csv https://github.com/bbchallenge/bbchallenge-undecided-index/b...
FartyMcFarter 2y ago
What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.
- Tainnor 2y ago
  For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/12473136ebd2e811c9c929c11522af5a32d603fb/Mathlib/Computability/Halting.lean#L219-L234 https://github.com/leanprover-community/mathlib4/blob/124731...
anon291 2y ago
Formal verification (i.e., automated theorem proving) relies on only admitting 'total' programs, which usually requires that any potential sources of 'bottom' (i.e., non-termination) come equipped with a proof that that never happens (usually based on well ordering of some structural decomposition in the recursion). Thus, most theorem provers are not turing complete and explicitly ban any turing complete structures. So, the various things they show and prove cannot be said to encompass all programs.

tsimionescu 2y ago

> We have lots of formally verified programs that show useful work can be done here. Yes, by restricting things to a non-Turing Complete subset. > Also, theoretical quantum computers can solve whether a problem halts 100% of the time. That is absolutely not true. Quantum computers are proven to be entirely equivalent to classical computers in terms of what problems they can solve. The only difference is that they seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.

lou1306 2y ago
> Yes, by restricting things to a non-Turing Complete subset. No, not necessarily. There are procedures that _can_ verify properties against Turing-complete and even infinite-state systems. It's just that no _general_ (as in, sound and complete) procedure can exist.
- tsimionescu 2y ago
  If it's not sound, than the result is meaningless. If it is not complete, then it only works on a subset of problems, which is equivalent to what I said.
  - lou1306 2y ago
    Agree that soundness is desirable, but "it only works on a subset of instances" and "you are restricted to a non-Turing complete subset" are not equivalent in the slightest.
    - deleted 2y ago
      [deleted]
    - lostmsu 2y ago
      Not sure what are you trying to say. Surely the "subset of instances" is non-Turing complete.
isaacfrond 2y ago
huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one? <citation missing>
- tsimionescu 2y ago
  I'm not sure what you're asking about. It is well known that certain computations can be determinstically proven to halt - there's even a prigramming language that only accepts programs that do so, Idris. Of course, not any computation can be written in such a way. But it's clearly possible to write certain programs in such a way that they must halt by construction. You can even do it in C: don't use goto, only use loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i < 100; i++) is ok, as long as i is not modified in the body), don't use in-line ASM, don't use recursion, don't use stdlib functions (definitely no string functions). These rules can be verified syntactically (+- problems with UB), and the resulting program is guaranteed to halt. But there are problems for which you can't write such a program. As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.
  - Tainnor 2y ago
    > there's even a prigramming language that only accepts programs that do so, Idris. If you declare every function total. Idris still allows partial functions, and you can even cheat the whole system with "assert_total". Of course, with some sort of linter, you could still make sure that everything is actually total (although technically, in Idris "total" doesn't necessarily mean "halts" - programs which generate infinite input are also total in Idris).

frabert 2y ago

> We have lots of formally verified programs that show useful work can be done here Yes, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.

darby_nine 2y ago

Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm. Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages. Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time. If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are. It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.

bionhoward 2y ago
Relevant video about MIP*=RE https://youtu.be/2H8629BCbkM https://youtu.be/2H8629BCbkM
- ykonstant 2y ago
  Lovely video!
arethuza 2y ago
Also worth noting that, from a practical perspective, even very simple programs/TMs can exhibit very complex behaviours that make it difficult to work out whether they will actually halt or not. At the time of writing there are 2833 5 state binary TMs that haven't been decided yet: https://github.com/bbchallenge/bbchallenge-undecided-index/blob/main/bb5_undecided_machines.csv https://github.com/bbchallenge/bbchallenge-undecided-index/b...

FartyMcFarter 2y ago

What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.

Tainnor 2y ago
For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/12473136ebd2e811c9c929c11522af5a32d603fb/Mathlib/Computability/Halting.lean#L219-L234 https://github.com/leanprover-community/mathlib4/blob/124731...

anon291 2y ago

Formal verification (i.e., automated theorem proving) relies on only admitting 'total' programs, which usually requires that any potential sources of 'bottom' (i.e., non-termination) come equipped with a proof that that never happens (usually based on well ordering of some structural decomposition in the recursion). Thus, most theorem provers are not turing complete and explicitly ban any turing complete structures. So, the various things they show and prove cannot be said to encompass all programs.