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