If your language is not Turing Complete, then it might be possible to always prove certain properties of programs. Canonically, you might be able to prove that

If your language is not Turing Complete, then it might be possible to always prove certain properties of programs. Canonically, you might be able to prove that the program will always complete and exit in finite time on any input. Other properties include guaranteeing that an error will not be thrown (or will be thrown), or bounding the amount of time or memory consumed, or guaranteeing that the output of a function will be within a certain numeric range.