You say that type mismatch errors are orthogonal to testing. This may be the case in languages like Java, which has a strong but not very expressive type system

You say that type mismatch errors are orthogonal to testing. This may be the case in languages like Java, which has a strong but not very expressive type system. In strongly typed functional programming languages like ML and Haskell, though, you can, with a bit of good design, capture a lot of information about what you want your program to do in the type system, to be checked automatically. Take, for example, the comment on this page by somebody who says that the only testing s/he does is XHTML validation. With strongly typed functional programming, it is possible, and not really even all that hard, to write an embedded combinator library for XHTML such that programs that generate improper XHTML don't type check in the first place.