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