3 ms·
> and of course it has a flexible type system that is actually sound, ... No holes! And this is where I went from "good faith reading" to actually not believin
by vorpalhex 6y ago
> and of course it has a flexible type system that is actually sound, ... No holes!
And this is where I went from "good faith reading" to actually not believing the article. Every general language that has made this claim has had holes - and those holes are usually patchable, but to claim a language with almost no adoption is leak proof is foolhardy at best. Just because you haven't discovered how your particular abstraction is broken doesn't mean it isn't.
- norswap 6y agoCopy/pasted from google search: > A sound type system means you can never get into a state where an expression evaluates to a value that doesn't match the expression's static type. It's not actually that hard to make a provably sound type system. The claim can only strain belief if it includes some type-level feature that makes this difficult. Of course, it should also be proved. e.g. Java's type system is not sound even though there is no good design reason while it shouldn't be (to be fair - it only happens in cases so intricately twisted that nobody will ever stumble on them by accident).
- CJefferson 6y agoIf you had gotten a bit further, you would have seen the type system is so amazing it stops you "misinterpreting data". Truely the future has arrived.
- vmchale 6y agoSoundness has a technical meaning. Point is, the type system at least isn't a shaky foundation.