F-Star [0] and Idris [1] are two great languages which give you a large variety of static analysis, and yes, provide ways to prove totality.
Idris, for instance, disallows recursion unless it can prove an argument "smaller" in the recursive call. For instance:
fib : Nat -> Nat
fib Z = Z
fib (S Z) = (S Z)
fib (S (S n)) = fib (S n) + fib n
In this case, the function pattern matches on natural numbers (Z stands for Zero and S for the one plus some other natural number). Each recursive call of `fib` has an argument which is smaller (closer to the base case), and thus this program must halt. Idris will not compile unless it can prove the program will halt. It, therefore, rejects all programs which would have halted but which it could not prove.
Idris, for instance, disallows recursion unless it can prove an argument "smaller" in the recursive call. For instance:
In this case, the function pattern matches on natural numbers (Z stands for Zero and S for the one plus some other natural number). Each recursive call of `fib` has an argument which is smaller (closer to the base case), and thus this program must halt. Idris will not compile unless it can prove the program will halt. It, therefore, rejects all programs which would have halted but which it could not prove.[0] https://www.fstar-lang.org/
[1] https://www.idris-lang.org/