With the property of verifiably correct behavior
> compiler plugin
A number of languages allow it (Haskell being the most prolific example, but also Java, Scala, gcc, many others)