For example, these (obviously inefficient) functions always terminate for all values of x, since both terminate given an input of 0, and 0 is the minimum possible input to these functions.
bool even(unsigned int x)
{
return (n == 0) ? true : odd(n - 1);
}
bool odd(unsigned int x)
{
return (n == 0) ? false : even(n - 1);
}While statically verifying your snippet is possible, it is also significantly more difficult to do than enforcing rules like "all loops must have an upper limit". I also think that you'd need dependent types to make this approach viable. Your simple example is IMHO rather an exception, just having "unsigned int" parameters / return types would mostly not suffice to statically verify that a recursive method will finish or not. (plus things like global state etc.)
But it's not the only way to get a total language (that always halts), contrary to what your original comment claims.
Neither language is Turing complete.
Programs with a fixed amount of execution time always terminate. That’s why we add timeouts to executions, because they’re a solution to the halting problem, which guarantees execution flow of our machines always returns at some point.