Okay, I think I understand now. My intuition was that "soundness" refers to whether the compile catches all invalid usage of types, and that soundness if violated if that doesn't happen; it sounds like the way you're using the term is measured whether the invalid usage is caught either at compile-time or run-time, and soundness if violated if it's not caught by any of the checks. I don't know whether my narrower understanding of soundness is incorrect or not, but it's at least more clear to me now why you grouped Java and JavaScript differently in terms of soundness.