[Prev][Next][Index][Thread]
safety and types
>From what I can tell there is actually some agreement on the following:
Safety and (practical) type systems are orthogonal language issues.
Safety is a property that the run-time system guarantees.
Type systems are proof systems that can establish that **some**
*implementation errors* in a safe language cannot happen. As C
demonstrates, types alone don't mean anything.
Mark, Jon F, and Jon R and a couple of private emails have brought up
additional issues concerning types, which I never raised.
program design: those of you who know what I have been up to recently know
very well that our new book for beginning programming is based on
type-directed function design (though we use Scheme because we believe it
has advantages over Haskell and ML). I won't argue this point (for now).
run-time ?!?!?!: I spent my sabbatical at CMU in 93/94 and had many
discussions on what this run-time thing really is (Jon F's words,
roughly). Bob and John convinced me that I shouldn't use the word type in
this context but "tagging" or "variant tagging". I happen to agree with
them.
abstraction: Jon R and also Jon F seem to suggest that a syntactic type
discipline adds some abstraction power to the language. I disagree,
and I will post a note on this but under a separate heading.
-- Matthias