[randomdata]

> C’s type system is unsound

Along with every other programming language under the sun. A complete type system is not exactly an easy feat – especially if you want it to be usable by people.

> We cope with this by referring to some code as “not type safe”.

Value constraints are an application of types, so yes, if C/Go had value constraints then violation of those constraints would leave it to not be type safe. But they don't have value constraints. Insofar as what the types can constrain, the safety is preserved.

It seems all you are saying is that C (and Go) do not have very advanced type systems. But that shocks nobody. Especially in the case of Go, that was an explicit design decision sung by its creators. You'd have to be living under a rock to not know that.

Was there something useful you were trying to add?

[cmrx64]

> Was there something useful you were trying to add?

Yes, the clarification about value safety, which you’ve done quite well.

Not every language is unrepentantly unsound.

I continue to identify a confusion in this thread between a property of the languages, and a property of particular code, but I have clearly exhausted your patience. thank you.

[randomdata]

> Not every language is unrepentantly unsound.

For sure. Coq does a decent job, but it's also a complete bear to use. Tradeoffs, as always.

> I continue to identify a confusion in this thread between a property of the languages, and a property of particular code

Go on. The original statement was that C and Go do not have type-safe enums. But there is no evidence of that being the case. The types are safe.

Indeed, the types are limited. An integer type, for example, cannot be further narrowed to only 1-10 in these languages. But the lack of a feature does not imply lack of type-safety. It only implies a lack of a feature.

[cmrx64]

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.