Hacker News Reader

> I really don't think this is the meaning of 'type-safety' in common parlance.

The bulk of the article is a call for more accurate use of terminology, so in a sense you’re noting the same thing: people using “type safe” when they mean “compile-time type-checked”, as a specific misuse of terminology.

The Wikipedia page spells out the difference clearly: https://en.m.wikipedia.org/wiki/Type_safety

Types are safe if they are checked, and the checking can be done statically at compile time or dynamically at run time.

Perhaps we’re just so used to working with type-safe languages that it is taken for granted (it would be quite unusual in eg Web Dev to use a language that is not type-safe) that the terminology is repurposed to be useful in conversations that we might have more often, eg, whether to rely more on static vs dynamic type checks.

> The author seems to want 'type-safety' to mean that it is made sure that an integer in memory is not accessed as if it were a float. While this is clearly a desirable feature that also dynamically typed languages provide by checking and/or converting at run time I really don't think this is the meaning of 'type-safety' in common parlance.

The author is wonderfully clear on this point. Under what he calls “Saraswat type safety” (not the best name), a dynamically typed language is type safe. So is a language like B that just has a word type (sort of... B may or may not have had UB depending on your perspective and UB may or may not preclude type safety... again depending on perspective).

There is a modern new-age use of the term “type safety” that means something less precise than this, namely your idea that it somehow precludes dynamic type checks. What nonsense. If a language checks array bounds dynamically, does that mean it’s not type safe? Give me a break.

> If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this possible or desirable.

It is not only possible, it is how dependently-typed languages/proof-checkers like Agda work.

The question is whether the performance hit that one gets from running such a language at run time is acceptable. For one, thing, it pretty much forces one to use a purely functional language. Which may or may not be a good thing.