Re: type safety


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?

Thanks,
Macneil

> From: Matthias Felleisen <matthias@ccs.neu.edu>
> To: Macneil.Shonle@sun.com
> Cc: com3810@ccs.neu.edu, robby@ccs.neu.edu
> 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
> 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:47:41 EST