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.