the disagreement is that the program is typesafe just because it was typechecked. BECAUSE the system is unsound (completeness is irrelevant), typechecking doesn’t imply type safety.

… where I am using type safety to mean “no runtime type errors/UB manifest”, ie, the property that a sound typesystem would guarantee _if we had one_. You seem to be saying that just because our type system is impoverished, does not make its resulting claim of “program is type safe” any less valid, whereas I am saying “type safety is a semantic property of programs, not of languages, and this value safety idea seems like it’s what PLTers think type safety means”.

It’s a violation of the C semantics to assign the wrong value to an enumeration, so I would say that fact the language doesn’t do anything at all to enforce or check this promotes this beyond “lack of a feature” and straight into “type unsafe”. However, I’d feel less strongly if at least initializers were checked.

As you say, different language design philosophies lead to this, and it’s not surprising. Most of these ideas came _after_ C anyway!

phone dying… no response soon.