Sussman, Robustness, & Quickcheck

Today on reddit there was a link to a paper by Gerald Sussman about how to construct robust systems.
If I understood correctly, his thesis is that one can only gain the robustness of biological systems by emulating their development: evolution and exploratory development. Not only that, but an emphasis on runtime tests and checks can help catch problems and further improve the strength of the system.

The idea makes a lot of sense when I think about it, but I have a feeling a lot of people who read it are going to take it as an argument for dynamically typed tools. It may have even been intended as such, but I do not presume to know the mind of Prof. Sussman.

On the other hand, I think a truly powerful type system may in fact help with exploratory programming and test-driven programming. When reading the paper I couldn't help but think of the beautiful Haskell system, QuickCheck. QuickCheck actually comes with GHC, so if you're using that compiler then you don't have to worry about installing anything else.

I actually think it'd be nice to have another example than the intro to the wiki, so I'm including my own stupid one: attempting to verify that a breadth-first search doesn't suck given that I already have some search that I know works.

>import Test.QuickCheck

>data Tree a = Node a | Branch (Tree a) a (Tree a)
>       deriving Show

So here we've defined a very simple binary tree, yay!

>dfs :: Eq a => a -> Tree a -> Bool
>dfs a (Node x) = a==x
>dfs a (Branch t x t') | x==a = True
>                      | otherwise = dfs a t || (dfs a t')

>bfs :: Eq a => a -> Tree a -> Bool
>bfs a tree = bfh tree []
>    where bfh (Node x) [] = x==a
>          bfh (Node x) (l:ls) = if x==a then True else bfh l ls
>          bfh (Branch t x t') l = if x==a 
>                                   then True 
>                                   else bfh (head l') (tail l')
>            where l' = l++[t,t']

Now we have two very simple forms of search. Let's now assume that God himself has descended and told us that our depth first search is The Awesome but we are worried that the breadth first search doesn't work. QuickCheck to the rescue!

>instance (Arbitrary a) => Arbitrary (Tree a) where
>    arbitrary = oneof [do
>                         x <- arbitrary                   
>                         return (Node x),
>                       do
>                         t <- arbitrary   
>                         t' <- arbitrary   
>                         x <- arbitrary   
>                         return (Branch t x t')]

>prop_Search t x = dfs x t ==> bfs x t

So here we've defined an instance of the Arbitrary type for our binary tree, and the property we check is that if the depth first search for a random element in a randomly generated tree is true then the breadth first search for that same element in that same tree must be true.

Of course I think we can go a lot further than this when it comes to exploratory programming and testing. I personally believe that a very strong static type system can help create a very tidy embedded language for genetic programming, but all I have are some very old toy examples on that front. Who knows how well we can do if we invoke Conor's Law?