[joshuamorton]

> Java does have a formal semantics, with a whole chapter on its soundness.

No, there's a chapter on the soundness of its type system. The spec being sound and the type system being sound are very different things. If we consider typescript to be JS's type system, then JS's type system is unsound. If we consider cpython in isolation, under the definition you're using, cpython cannot be unsound, as it is untyped, QED.

If you're talking about whether the language's type system is sound, asking "These documents are just informal prose. Are they sound?" isn't even a well defined question.

> I'm not criticising Python as being exceptionally bad, but we can certainly do it much better.

You absolutely were when you said "But I wish Ruby and Python were this explicit and easy to understand!"

[chucke]

You're arguing with the guy who did truffleruby. I'd say he knows a thing or 2 about the soundness of dynamic languages and adhering to a formal spec.

[xx_ns]

Argumentum ab auctoritate.