On Tuesday, 21 November 2017 at 06:03:33 UTC, Meta wrote:
I'm not clear on whether he means that Java's type system is unsound, or that the type checking algorithm is unsound. From what I can tell, he's asserting the former but describing the latter.
He claims that type systems with existential rules, hierarchical relations between types and null can potentially be unsound. His complaint is that if Java had been correctly implemented to the letter of the spec then this issue could have led to heap corruption if exploited by a malicious programmer.
Runtime checks are part of the type system though, so it isn't unsound as implemented as generated JVM does runtime type checks upon assignment.
AFAIK the complaint assumes that information from generic constraints isn't kept on a separate level.
It is a worst case analysis of the spec...
