I put together a small intro lesson on proving haskell code using quickcheck, equational reasoning and Isabelle/HOL. Its very elementary, but might be of interest to some people here. http://www.thenewsh.com/%7Enewsham/formal/reverse/ Feedback is appreciated. Tim Newsham http://www.thenewsh.com/~newsham/