Java isn't sound and the poor semantics of null are critical to proving it.
Not that this takes away from your larger point exactly, but Java+null is no longer a good example.
Not that this takes away from your larger point exactly, but Java+null is no longer a good example.
* It turns out Java accidentally turned out to be unsound in a really obscure corner case, unrelated to the nulls thing. https://hackernoon.com/java-is-unsound-28c84cb2b3f
Java has always had covariant arrays, which are not sound. Whether it was intentional or not is irrelevant to the question of 'does this language have a sound type system?'.
As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?
If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.