&gt; Learning to do advanced kinds of static verification with Haskell&#x27;s type system is actually rather difficult<p>Perhaps. But it benefits greatly from being a consistent way of doing things: everyone does their static verification the same way, because the language supports exactly one way of doing it.<p>&gt; and usually requires language extensions.<p>Sometimes. But again at least those extensions are relatively standardized, rather than completely ad-hoc as a macro can be.<p>&gt; Indeed, Haskell programmers often use QuickCheck to do ad-hoc verification of type class laws, for example, since they can&#x27;t be proven in the type system.<p>Yeah, that&#x27;s one of the reasons I&#x27;m excited about Idris. But even in your example, QuickCheck is again a standardized way of doing this.