That they are always terminating is very useful for programs that generate proofs, or otherwise don't have to be evaluated.

But if you can encode the Ackermann function, proof of termination is not very useful in practice - as it may consume arbitrarily large amounts of space and time to evaluate (easily more than the age/size of the universe).