Subject: Re: type safety
From: Macneil Shonle (Macneil.Shonle@Sun.COM)
Date: Mon Feb 04 2002 - 10:47:38 EST
Thanks for the clarification! So, if a typed program doesn't go wrong as often,
then that means sometimes it *does* go wrong. If it can't be a type error and
it's not a user error (taking a car of an empty list...), then the only thing
left is compiler errors? This can be seen as an issue with Java: so what if it's
type sound if the VM has bugs?
> From: Matthias Felleisen <firstname.lastname@example.org>
> To: Macneil.Shonle@sun.com
> Cc: email@example.com, firstname.lastname@example.org
> Subject: Re: type safety
> 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
> By C/C++ going wrong I mean something much worse than the above. I mean
> this. The programmer writes down
> int x;
> 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
> -- Matthias
This archive was generated by hypermail 2b28 : Mon Feb 04 2002 - 10:47:41 EST