Your first point runs counter to my understanding of what the author said. Specifically: "Here’s our “true” unsoundness example that has been making the rounds

Your first point runs counter to my understanding of what the author said. Specifically: "Here’s our “true” unsoundness example that has been making the rounds most recently. It assigns an Integer instance to a String variable. According to the Java specification, this program is well-typed, and according to the Java specification it should execute without exception (unlike the aforementioned backdoors) and actually assign the Integer instance to the String variable, violating the intended behavior of well-typed programs. Thus it illustrates that Java’s type system is unsound." That is, the author's unsoundness claim is independent of the class cast exception. On your second point, you may be in violent agreement with the author. What is the difference between "a weakness in the specification" and being "unsound"? The author's definition is that this is an unintentional hole in the type system, unlike the intentional ones he outlined.