3 ms·

Mostly good points but also some quibles. "Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code."

by cjfd 7y ago

Mostly good points but also some quibles. "Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code." 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. Maybe the best way to program is to have specifications in a language as close to mathematics as possible and executable code in a language much closer to the machine. It is not clear to me that both of these things should be the same language. "Equivocating around type-safety" 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. If I attempt to use a variable as if it were of a different type I generally get a runtime error in a dynamic language, e.g., because I am accessing a field that does not exist. 'type-safety' is the property that the language prevents this runtime error from happening because this is checked at compile/lint time.

DougBTX 7y ago
> 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 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.
pizlonator 7y ago
> 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.
rntz 7y ago
> 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.
- cjfd 7y ago
  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.

by cjfd 7y ago

DougBTX 7y ago

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

pizlonator 7y ago

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

rntz 7y ago

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

cjfd 7y ago
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.