SPARK (Ada) has compile time pre and post conditions, and it works well. If you declare the post-condition Collatz (n) = 1, the compiler can't help you, and compilation will fail. If you've got a difficult condition, you're going to have to help the theorem prover, often by introducing "ghost" functions, or by simply softening the condition. In the latter case, you can't prove total correctness, but you can often still prove things like absence of run-time errors.