> It's not just that "there is more", it's that there is everything. The halting problem ....
No, no, no. The original halting theorem is avoided in total languages, but the much more important version which forms the core of the time-hierarchy theorem, sometimes known as "bounded halting", holds unchanged. It is a generalization of halting which basically says that you cannot know anything about a program (including halting) any faster than running it (more precisely, you cannot know whether a program P halts in input x within n steps in fewer than n steps; all the other corollaries like Rice follow in the same way). This means that the cost of verification is the same for total and non-total programs, with the theoretically interesting but pragmatically irrelevant promise that the cost is some unbounded finite number in the total case.
If you want to convince yourself that totality cannot make proving program properties easier with an intuitive argument, consider this: take any program ever written, and to every loop and every recursive call add a counter initialized to 2^100 that is decremented with every iteration/recursion and stops the program when it reaches zero (which will not happen until the end of the universe). Your program is now provably total, yet its semantics have not changed a bit. I.e., you can already assume without loss of generality that every program is a total program and that every language is a total language. Is verification easier now that you know this?
The only case where you cannot make this assumption is when your language is used as a theorem prover to prove general mathematical theorems (that aren't executed and may actually "reach" infinity), and this is where totality matters.
No, no, no. The original halting theorem is avoided in total languages, but the much more important version which forms the core of the time-hierarchy theorem, sometimes known as "bounded halting", holds unchanged. It is a generalization of halting which basically says that you cannot know anything about a program (including halting) any faster than running it (more precisely, you cannot know whether a program P halts in input x within n steps in fewer than n steps; all the other corollaries like Rice follow in the same way). This means that the cost of verification is the same for total and non-total programs, with the theoretically interesting but pragmatically irrelevant promise that the cost is some unbounded finite number in the total case.
If you want to convince yourself that totality cannot make proving program properties easier with an intuitive argument, consider this: take any program ever written, and to every loop and every recursive call add a counter initialized to 2^100 that is decremented with every iteration/recursion and stops the program when it reaches zero (which will not happen until the end of the universe). Your program is now provably total, yet its semantics have not changed a bit. I.e., you can already assume without loss of generality that every program is a total program and that every language is a total language. Is verification easier now that you know this?
The only case where you cannot make this assumption is when your language is used as a theorem prover to prove general mathematical theorems (that aren't executed and may actually "reach" infinity), and this is where totality matters.
See my post for a more in-depth discussion: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...