The QuickCheck style of testing is my favorite (see paper [1]). Using a simple embedded DSL, you write specifications that declare the desired properties of you

The QuickCheck style of testing is my favorite (see paper [1]). Using a simple embedded DSL, you write specifications that declare the desired properties of your code. The computer then checks that the properties hold by randomly sampling the space of possible test cases, using one of several sampling strategies. Even though the checks are not proofs, they are very effective in practice. For example, here's a quick Haskell session in which I claim that the function f has the property of returning its smaller argument: Prelude> import Test.QuickCheck Prelude> let prop_minWins x y = if x < y then f x y == x else f x y == y Prelude> quickCheck prop_minWins +++ OK, passed 100 tests. The best part is that the property specifications are not only machine testable but human readable. They allow you to tell other humans what you code should do, using a clear, formal language that the machine can check to make sure you didn't tell any lies. For example, the second line in the code sample above says, "For all x and y (which are values of some type on which there is a less-than relation), if x < y then f(x, y) = x; otherwise, f(x, y) = y. See [2] for another great example. [1] http://www.eecs.northwestern.edu/~robby/courses/395-495-2009-fall/quick.pdf http://www.eecs.northwestern.edu/~robby/courses/395-495-2009... [2] http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-ParserCombinators-ReadP.html#g%3A5 http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-Pa...