Re: type safety


Subject: Re: type safety
From: Matthias Felleisen (matthias@ccs.neu.edu)
Date: Mon Feb 04 2002 - 10:30:17 EST


Nobody will include limitations such as finite memory or finite
arithmetic. People always assume certain idealizing assumptions.
I consider this justified, and don't know anybody who doesn't.

Milner had in mind type errors:
 - applying a boolean or numeral
 - if-testing a numeral or a function
That is, he was thinking of "big" domain mismatches that come up
within Scheme or some other "untyped" version of the same language.

He (perhaps intentionally) chose not to work with a language that included
division, array dereferencing, list access, etc. As a result, he could
literally formulate the slogan as

 "Typed programs don't go wrong."

Later on, ML people used to say that a typed program may raise exceptions,
but that it won't trigger an error. The enlightened part has given up on
that. They now admit that it is pointless to distinguish between errors and
exceptions.

By C/C++ going wrong I mean something much worse than the above. I mean
this. The programmer writes down

 int x;

and

 char y;

The C/C++ type checker may bless this program but that does not mean that
during program evaluation the char y doesn't get assigned bits from the int
x or some such things. In other words, according to the programmer's
declarations, the computation may proceed after performing such a
misinterpretation without ever signaling anything, with an error that shows
up much later, possibly in the form of a core dump or bus error, etc.
In short, type checking means nothing for the execution of the program and
when you get an error it does not eliminate any possible cause for the
problem, including Milner's type errors (when seen from the programmer's
perspective).

-- Matthias

 



This archive was generated by hypermail 2b28 : Mon Feb 04 2002 - 10:30:18 EST