There are different ways to check whether a program is “cor- rect”, including dynamic testing and static type checking. Unfortunately, testing only checks a certain (finite) set of inputs and types may be too imprecise to express complex correctness properties. For example, correctness of a sort- ing routine requires that the output is both sorted and con- tains the same elements as the input. Program verification aims to prove such correctness properties for all possible in- puts based on annotations such as pre-, postconditions, as- sertions and invariants. However, the verification process for these annotations can become complex. Therefore, sim- ple error messages may not be sufficient to help the pro- grammer understand and resolve verification issues.