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

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