3 ms·
There is still an even more subtle point that you are absurdly close to understanding, and that the article touches on a bit — there really is no such thing as
by blasdel 16y ago
There is still an even more subtle point that you are absurdly close to understanding, and that the article touches on a bit — there really is no such thing as a type system, only a set of times and places where types are(n't) checked — operations. You even say so yourself!
You'll find programming language theorists using the phrase "a sound subset" with no qualms.
- deleted 16y ago[deleted]
- derefr 16y agoSaying that there is no such thing as a type system is like saying there is no such thing as an integer. Sure, your machine can only represent an integer (and not very well), but that doesn't mean they don't exist—they're simply mathematical constructs. Mathematical constructs can have properties, such as being prime or composite, real or transfinite, countable or uncountable, or, in this case, strong or weak. > You'll find programming language theorists using the phrase "a sound subset" with no qualms. It makes no sense, though. There is no sound subset of C, because C isn't checked anywhere. There is no amount of pruning you could do that would allow you to call the result "sound": only by adding checks could you assert that. The usefulness of the term "strong" is that a strong system (pure surjective digraph) is able to be made sound, while a weak system (impure digraph) is not.