One option which allows you to keep Turing completeness is just asking the user to write more annotations, such as loop invariants and termination conditions. For example the Dafny [1] language+verifier does this: it automates the tedious parts of the proofs but requires the user to give the hard parts (loop invariants) as annotations.