You can compromise on turing-completeness, too. Idris, for example, lets the programmer decide whether a given definition should be required to provably terminate or not.