Type System vs Test Driven Development

All code is a trivial recombination of working parts. It's all CPU opcodes in the end. Haskell's guarantees may extend a bit further but if your program isn't trivial it still needs testing, if only to verify that the program does what you think it does. I'm fiddling around with porting my HTML normalizer into Haskell, and even if the type system reliably lets me say "Hey, this has no type errors" and gives me some reasonably assurance based on the way it is written that it has no infinite loops (not a proof, but there's not very many places they could hide), I still need tests just to make sure it does what I think it does. A lot of them, actually.

That's weird, because Haskell has great unit testing tools. I'm especially fond of QuickCheck, which allows me to define algebraic properties of functions:

xs == reverse (reverse xs)

QuickCheck will generate hundreds of random lists and make sure that the property holds. This can be enormously useful in smoking out odd problems in complex functional code.

For simpler testing scenarios, HUnit is OK, although it sometimes feels a bit clunky.

One of the interesting recent developments in Haskell testing is the creation of automated proof tools for Haskell programs. Will Sonnex presented Zeno [1] at AngloHaskell 2010, and while it still has limitations in terms of the language features covered, it's a fascinating glimpse into where software testing might go.

[1] http://www.doc.ic.ac.uk/~ws506/tryzeno/

These posts about how a type system can guarantee correctness always make me a little envious of the poster. Not envy that their work isn't hard, but that it has a kind of straightforwardness, with problems so well-defined that a proper analysis guarantees you've solved it completely.

In my work, the types are usually so nailed-down there isn't any question about them. Yet the problems can be so nonlinear and ill-conditioned that even moderate testing-- say, hitting the code with 1000 test cases-- is just not enough to convince myself it's working correctly. It often happens that a unit test runs just fine at that level, but bumping it up to 10,000 or 100,000 cases reveals weaknesses in the code.

Illustrative example follows-- no need to read if you "get" that, in some fields, a type system simply doesn't detect the interesting bugs. A few months ago, I was testing methods for solving problems of sorption to room surfaces. In terms of types, it could hardly get more explicit. Take an object representing a sorption isotherm, plus two double-precision numbers giving gas- and sorbed-phase concentrations, and return the equilibrium concentration at the sorbent surface. The only way to specify the types more completely would be to tag all the numbers involved with units.

Guaranteeing convergence turned out to be a royal pain. To get a useful answer, you need to force convergence to very tight tolerances-- tight enough that, on ill-conditioned problems, you run the risk of asking for answers below the machine precision. That means you need two termination tests-- one on the defining equation (is the error close enough to zero?), and one on the returned result (is the current best answer within a tight enough bracket?). And within that framework, it's very easy to create algorithms that, due to finite-precision effects, fall into infinite loops because they fail to actually change a bracket point when they add a small number to it.

So again, types were not an issue. The only way I was sure I had all the convergence pitfalls out of the way was extensive unit testing. And the baby tests I ran during initial development-- sampling 1000 combinations out of a database of sorbents and chemicals-- simply didn't do it. Once I had "working" code, and stepped up sampling to the 100,000 range, it was easy to discover oddball combinations that would cause problems.

I'll never understand how people can equate type correctness with value correctness, regardless of the language.

I feel like this guy must not have to parse binary very often.