> 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.
> 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.
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.
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.
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>
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.
> 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).
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.