in response to chalst, and further on the topic of type systems:

there is no deep theoretical difference between static and dynamic type systems. you are still talking about writing a specification (program) in which the computer may do something you do not expect or desire. the only practical question worth asking is: how much confidence do you have that the specification you wrote will get the computer to do the thing that you, or your customers, want?

testsuites test some cases. type systems check consistency. the assumption is "consistency implies correctness", and it's hard to come up with much better definition for correctness than both "testsuite pass" and consistency; in practise this is as close to true as we get.

I've used many C and lisp systems professionally, and a few HM systems, and the HM systems are by far more designed around consistency checking. you can consistency-check lisp if you have the luxury of using ACL2 or a vendor compiler with a deep partial evaluator or soft-type inferencer. but usually in lisp you are working on a lousy implementation, with an OO or struct system someone threw together for fun, and less checking even than the "disjointness guarantee" inherent in fundamental scheme types. likewise in C you are not usually working with a larch or lclint-annotated system; you've got a system which "made up" an OO type system on top of liberal pointer casting, and not a hope in hell of checking its consistency. C++ thankfully has a good type system, but as the original article points out it can get pretty brutal to compile.

the more checking I can perform before I ship something to a customer, the better. imho everything else is religion and bafflegab. ocaml and haskell currently give me lots of good checking without taking away too much, so I use them when I can.