[joshuamorton]

> That's great! Can you point me at the formal proof? I haven't seen it myself.

Can you point me at the proof for the soundness of the documented behavior java or javascript or C++ docs? A cute little table isn't a substitute for soundness, and none of the languages you mentioned are mores soundly implemented (at least in their popular implementations).

> It's easy to see where these simple English descriptions aren't covering everything. To give you a practical example - look at https://docs.python.org/3/reference/datamodel.html#object.__... - 'should return False or True' - what if it doesn't? Where's that specified? Is it somewhere else in this document? That's the kind of practical issue we work with when implementing languages.

Cpython raises an exception, and in general, cpython is the spec unless otherwise specified is how things turn out.

> How can you test against English prose? You can't. So someone's manually translated the prose into tests elsewhere I guess. Have they done that correctly? How can we verify that? Was there any ambiguity when they were interpreting the English?

This is sort of a silly complaint. every spec is implemented in english prose[1]. That's why we end up with arguments about SHALL vs. MUST in the specs. Except in the rare cases where the spec is a test suite, which usually reduces to the case of cpython: the popular implementation is the spec (or maybe the popular implementation forks its test suite out into a different repo to make it more "independent")

[1]: Please don't make a irrelevant point about an obscure implementation of C that's implemented in agda and the "spec" is the proof of soundness or whatever, that's fundamentally the same as the implementation is the spec, especially given that said C implementation probably isn't ANSI compliant or whatnot.

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