Oh, I'm definitely not saying that it replaces automated testing. A mixed approach is almost certainly best. I like randomized testing, too. Just, (conservative

Oh, I'm definitely not saying that it replaces automated testing. A mixed approach is almost certainly best. I like randomized testing, too. Just, (conservatively) half of the things people write as unit tests could be expressed in the type system in OCaml* . If not correct for all possible input, they prevent the program from compiling, and lead you to everywhere the property doesn't hold. That's arguably a stronger guarantee than passing tests for known input->output at runtime. (In all fairness, much of it can also be done with Java or C++'s type systems, but without type inference it becomes incredibly tedious, and ML type constructors are far more direct than wrapping things in classes all over the place.) Type systems are also "just another tool", though, and more useful in some cases than others. I wonder how many other properties about a program could be declared, inferred, and verified for the complete domain of input at compile time -- this is safe to use concurrently, that is fully isolated from non-deterministic input, this can have its results memoized, those can fully evaluated once at compile time and don't even need to run in final executable, etc. (Haskell can do some of this, but I don't like lazy evaluation as a default, among other things.) Playing with Prolog and logic programming has gotten me curious about how far that sort of analysis could be pushed. About the insurance example -- I know exactly where you're coming from. I've done something similar for the architectural industry, and a huge suite of example results helped tremendously. * And very likely Haskell, SML, Clean, and others, but my "advanced type system" experience is mostly with OCaml.