This would make it impossible to compose mathematical expressions of more than one operation without discharging the Maybe which would get ugly fast.
Practically speaking, languages like Haskell and F# have a monadic syntax that makes this considerably less ugly.
Total functions have to return either true or false explicitly, failure as negation doesn't work.
That is where you get Gödel's 'this statement is false' from.
This is the law of the excluded middle that broke the Mathmatica Principia.
Plato, Aristotle, and Russell's use of the law of the excluded middle is what Gödel, Church, and Turning leverages.
For problems in P this distinction is harder to see because P=co-P but we think NP!=co-NP.
As NP are by definition decision problems this is important.
NP being the provable yes-instances and co-NP being the no-instances, even proving a function is total is hard.
If you accept failure as negation you may be able to build a sun-Turing machine that always halts but you won't be able to show it is complete and consistent.
That is why ZF disallows statements like 'this statement is false'.
It's best left to the compiler.
But if you're considering doing it, don't imagine yourself taking an existing function like qsort and trying to prove it's total. Instead try building up a new function and only build it out of other total functions.
As all primitive recursive functions are provably total, that is a place a compiler can work. But just using for loops gets you there too.
Total functions that are also pure functions are a pretty small set so there may be other reductions like the above. But don't depend on the compiler.
But I agree writing total functions from the start is the ideal if possible.
For example, in Lean4:
def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat
:=
if denominator > numerator then
0
else
1 + myDiv (numerator - denominator) denominatorNotZero
-- Example usage.
example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl
example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl
I feel like you would just end up with the equivalent of Maybe, but not sure.
Just in time for people to ignore it and start complaining about the ugliness of flatMap from 2015 onwards.