3 ms·

I think it's just a knee jerk reaction to some academic/PL theory types that chime in with a "Huzza! Long live (Haskell/Scala/Ocaml/etc.)!" As if a lack of soun

I think it's just a knee jerk reaction to some academic/PL theory types that chime in with a "Huzza! Long live (Haskell/Scala/Ocaml/etc.)!" As if a lack of soundness is dawning on anyone and was anyone's issue to begin with. It's pretty dramatic so it gets met with preemptive defensiveness. From the end of article: Everything is broken. Everything is fine.

jerf 8y ago
In theory, as soon as a type system is unsound, it is unsound. In practice, there are ranges of brokenness. If you have to go hunting for the problem, and it takes a combination of 5 obscure features which nobody would ever use together, it's not that big a deal. If it's the sort of thing that you encounter in any non-trivial program, well.... ... your language dies. Part of the reason so many people in this thread can be cavalier about type soundness issues is precisely that all the languages they use, being the languages that did not die because they have a crappy type system, are pretty sound, within the model the language is operating under, so, yeah, of course it doesn't look like a problem to a normal programmer, because it was solved a long time ago. Doesn't mean it's a bad idea, or that people should just sneer contemptuously at the issues and snidely dismiss them as academic frippery, because then these people go on to write new languages that have these sorts of issues. (Like the recent wave of "event based" programming environments that just threw away the benefits of structured programming, because they were so thoroughly immersed in a structured programming world they didn't even realize how thoroughly they'd internalized it, had no idea what the preconditions were for it, and not only had no idea they were throwing it away but snidely berated people who pointed it out. And then spent 5+ years rediscovering it all over again....)

jerf 8y ago

In theory, as soon as a type system is unsound, it is unsound. In practice, there are ranges of brokenness. If you have to go hunting for the problem, and it takes a combination of 5 obscure features which nobody would ever use together, it's not that big a deal. If it's the sort of thing that you encounter in any non-trivial program, well.... ... your language dies. Part of the reason so many people in this thread can be cavalier about type soundness issues is precisely that all the languages they use, being the languages that did not die because they have a crappy type system, are pretty sound, within the model the language is operating under, so, yeah, of course it doesn't look like a problem to a normal programmer, because it was solved a long time ago. Doesn't mean it's a bad idea, or that people should just sneer contemptuously at the issues and snidely dismiss them as academic frippery, because then these people go on to write new languages that have these sorts of issues. (Like the recent wave of "event based" programming environments that just threw away the benefits of structured programming, because they were so thoroughly immersed in a structured programming world they didn't even realize how thoroughly they'd internalized it, had no idea what the preconditions were for it, and not only had no idea they were throwing it away but snidely berated people who pointed it out. And then spent 5+ years rediscovering it all over again....)