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
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).