Use a prover like [why3](http://why3.lri.fr/) in order to provide the ability to prove invariants about the logic of functions of the language in compile time.
Use a prover like why3 in order to provide the ability to prove invariants about the logic of functions of the language in compile time.