RE: dynamic vs. static typing

["Anton van Straaten" <address@hidden>]

Steve Dekorte wrote:
> On Nov 24, 2003, at 10:09 PM, Matt Hellige wrote:
> > There's one other interesting and important aspect: a well-designed
> > static type system provides a second perspective that is provably
> > complete in some relevant and well-specified way, as opposed to, for
> > example, unit tests. With unit tests, the responsibility for ensuring
> > (and understanding) completeness of coverage lies entirely with the
> > programmer.
>
> That's true, but only the programmer knows what the program is supposed
> to do. A missile guidance program can pass a static type check and
> still not guide the missile to the correct location. Of the almost
> limitless number of possible bugs, type checking (assuming few dynamic
> operations are done) eliminates, at best, a extremely small percentage.
> And that percentage is most likely a tiny subset of the very large
> percentage that testing eliminates.

Without early typechecking, the proportion of type errors which manifest
during testing and at runtime rises significantly - and often, their nature
isn't as clearly identified, so they take longer to track down.  Looking at
this in terms of what percentage they are of all possible errors is
misleading at best.

I'm reminded of the argument about wearing helmets on a bicycle or
motorcycle: head injuries actually aren't that high a proportion of the
injuries that occur during accidents, so why wear a helmet?  Of course, some
people do take that position, and that's a risk they may be free to take,
depending on local laws.  I suspect you'll find much less willingness to
take that position amongst the developers of missile guidance systems,
though.

Pierce has a nice description of the subjective effects of static type
checks, in TAPL:

   "In practice, static typechecking exposes a surprisingly broad range of
errors.  Programmers working in richly typed languages often remark that
their programs tend to "just work" once they pass the typechecker, much more
often than they feel they have a right to expect.  One possible explanation
for this is that not only trivial mental slips [...] but also deeper
conceptual errors [...] will often manifest as inconsistencies at the level
of types."

Anyone who's made serious use of a language with a good static typesystem
has experienced this.  Think of it as a way to get an entire class of
high-performance unit tests without having to actually write them.

Anton