[chrisseaton]

> Can you point me at the proof for the soundness of the documented behavior java or javascript or C++ docs?

https://link.springer.com/book/10.1007/3-540-48737-9

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

> in general, cpython is the spec

Well there we go - turns out the written document doesn't cover everything after all. A second ago we were at 'Every guaranteed behavior of python is described clearly and concretely in these documents.' Turns out not.

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

[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.