Re: type safety

Correct. I didn't split the cases enough: 

 1. Using a type system you can shift checks and errors from the language 
    interpreter to the program. I agree. 

 2. You admit that this is impractical. 

 3. You should also admit that it defeats the purpose of using types to
    prevent certain classes of errors. Now instead of the language
    enforcing it, we let the programmer struggle with an incredibly
    complicated type system and rely on the programmer to signal proper
    error messages. Is that an improvement? 

;; --- 

I don't know how you get the idea that I don't think types help me
eliminate certain classes of errors. I wrote 

  "[Types] help us prove that certain things are true about a program
   without running it. In particular, some type systems help us prove that
   a program won't viololate certain safety restrictions that they
   implementation imposes on computational operations."

And Jon Riecke didn't argue about rejecting programs (which I agree with,
kind of) but about representing pointers as integers (which I couldn't care
less about). 

As for abstraction, I claim that using a generative facility for structure
definition I can enforce the same abstraction constraints w/o syntactic
types (all programs run, safely) that you can enforce with types (some
programs get rejected, the others run safely).

-- Matthias