> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. I mean, you are hiding a lo

> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. I mean, you are hiding a lot of possibilities in "etc. etc.". So is the article, when it says "and the like" in the sentence you're referring to. The kinds of things that belong in this list are described as "generally some sort of safety property." That's a big big list of things. It's not a particularly strict or narrow definition of type system, IMO. Take C. What does it mean when C's type system says a variable "x" has type "int"? Practically, it means the compiler knows how many bytes (let's say 4) to reserve on the stack for x. But what if the program, during the course of execution, tries to write an 8-byte piece of data to x? The language is broken if that can occur because the compiler was not justified in reserving only 4 bytes for x. So, part and parcel of C's type system is a global safety property: It promises, among many other things, that at runtime no assignment will ever occur to an int-typed variable unless the assignment payload is 4 bytes. So this is exactly what the article is talking about. Local rules (e.g., "int x = y" is well-typed if y has type int) working together to guarantee a global safety property (no type mismatches can occur at runtime). The failure of a type system to do this properly is a failure at being a type system. And indeed, since C has undefined behavior, it's type system falls apart immediately. It's just not even interesting to consider enumerating the ways it can be broken. The type systems considered by this article are ostensibly supposed to not be broken the way C's is. That's what makes the counterexamples of this article so interesting.