I propose that haskell' include a standard syntax for invariants that the programmer wants to express. Here is a rough idea (just to get the point across): \begin{code} head :: [a] -> a head xs @ require { not (null xs) } head (x:xs) = x reverse :: [a] -> [a] reverse @ ensure { reverse (reverse xs) == xs } reverse [] = [] reverse (x:xs) = reverse xs ++ x data RedBlackTree a = RBLeaf a | RBNode Bool (RedBlackTree a) a (RedBlackTree a) invariant RedBlackTree a where RBNode False _ l _ r ==> redDepth l == redDepth r \end{code} The intent is not to have standardized checks on the invariants, its just to supply a common way to specify invariants to that the various strategies for checking them can all work from the same data. For example, one tool might use the invariants to generate QuickCheck properties, a compiler might provide a mode that does run-time checking of the invariants, and another tool might try to prove the invariants statically like in ESC [1]. Eventually, we might end up with sophisticated hybrid approaches that combine static proof with generating test cases for the unprovable bits. At the very least Haddock could include the invariants as part of the documentation. [1] http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps