Totality really mostly helps when using typed programming languages as proofs of general (non-executable) mathematical theorems via propositions-as-types. Without it, the logic will be inconsistent. For actual programs, though, it makes little difference.
Totality does in no way make proving correctness easier in practice. See http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
Totality really mostly helps when using typed programming languages as proofs of general (non-executable) mathematical theorems via propositions-as-types. Without it, the logic will be inconsistent. For actual programs, though, it makes little difference.