Impossible to prove for any arbitrary program doesn't mean impossible to prove for programs that we actually care about, and it especially doesn't mean impossible to prove for a program where the programmer is intentionally trying to write a program where certain attributes are provable.
Any statically typed language necessarily has to prevent some well-formed programs from being represented. This language would just need to reject programs where it can't prove the attributes that it is suppose to prove in addition to programs that are actually malformed.
It is really ergonomics that prevents a language like this from taking off, not any theoretical concerns. Languages that let you prove a lot of complex properties at compile-time take too much work to use, but they are not impossible to create.
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.
Any statically typed language necessarily has to prevent some well-formed programs from being represented. This language would just need to reject programs where it can't prove the attributes that it is suppose to prove in addition to programs that are actually malformed.
It is really ergonomics that prevents a language like this from taking off, not any theoretical concerns. Languages that let you prove a lot of complex properties at compile-time take too much work to use, but they are not impossible to create.