<li> Not as hard to use as I imagined.
-<li> Mostly useful for small functions.
+<li> Mostly useful for small functions. <br>
+<big>→</big> For large functions look at constructive proofs in WhyML.
<li> Forces you to think very hard about assumptions and corner cases.