It wouldn't be too bad if it was complicated, but explicitly documented and tested.

For example people joke about JavaScript comparison semantics posting things like this https://i.stack.imgur.com/35MpY.png and laughing about it. But I wish Ruby and Python were this explicit and easy to understand!

Python docs have pages on the execution model and data model, with notes in implementation details. What more do you want?

https://docs.python.org/3/reference/executionmodel.html

https://docs.python.org/3/reference/datamodel.html

Reading these documents is not hard, and it’s been an enormous help over the years for writing effective efficient Python.

> What more do you want?

Something formal, so I can actually reason about it and test it.

These documents are just informal prose. Are they sound? I don't know. Do you? Does anyone? Does my implementation match what they say? Who knows. Does CPython even match it? Does anyone know?

As an outsider this may be your perception, but this is not how python's documentation works.

> These documents are just informal prose.

Not true. They're the language spec. Every guaranteed behavior of python is described clearly and concretely in these documents.

> Are they sound?

Yes.

> Does my implementation match what they say?

Yes.

> Does CPython even match it?

Yes.

> Does anyone know?

Yes! There's a very rigorous and thorough set of unit tests that specifically test an implementation's ability to match precisely the behavior described in these documents. All implementations (that I'm aware of, eg. cpython, pypy, jython, etc) state which versions of the spec they are compatible with, in other words they pass the unit test suite for that version.

Further, the maintainers of python (and by that I mean, regular contributors to the python-dev mailing list, not a cabal of robed individuals in a cave somewhere) are deeply aware of the language of the spec, the way the test suite implements it, and the importance of maintaining this relationship.

>> Are they sound?

> Yes.

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

> There's a very rigorous and thorough set of unit tests that specifically test an implementation's ability to match precisely the behavior described in these documents.

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?

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.

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

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

> 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!"

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.

Argumentum ab auctoritate.

Out of curiosity, how many languages would meet those criteria? Only one I can think of off the top of my head is CompCert's C dialect. Are there others?

It's a spectrum - some languages do it a lot better than others. Not having anything more than a conversational English description of what it does is definitely the lower end of the spectrum. I'm sure very few are doing it perfectly, but for example Java has a formal semantics.

> but for example Java has a formal semantics.

I don't think that's really true. The Java language specification is entirely prose. The book you linked to was written by "outsider" authors and published in 1999 (!).

That was just one example of many - there's a whole cottage industry of writing formal semantics for Java.

https://fsl.cs.illinois.edu/publications/bogdanas-rosu-2015-...

None of them are official, and I bet they make major simplifications (the one you just linked to is for Java 1.4). I doubt actual language/tooling implementors benefit much from them.

Standard ML certainly has clear specifications and proofs of soundness of the type system.

Forget about language quirks, package management and version management in python is a nightmare. The ammount of time I wasted dealing with python environment related issues alone makes me avoid it if I can.

Have you seen the Python docs which have pages on the execution model and data model, with notes in implementation details?

https://docs.python.org/3/reference/executionmodel.html

https://docs.python.org/3/reference/datamodel.html

In your second link it says:

> For instance, to evaluate the expression x + y, where x is an instance of a class that has an __add__() method, x.__add__(y) is called.

The talk I linked to (https://youtu.be/qCGofLIzX6g) is a deep dive on how there is much more to the story than the simplified statement above.

What I wish for is not better docs, but rather simpler language in which the statement above would actually be an accurate specification of the behavior implemented by the interpreter.

I guess you are trying to imply that those documents cover a formal-enough description of what the execution and data model is. Well, even for the section "names" it just forgets to say if imported and non-imported names all share the same encoding and which should it be - just a nitpick, but with less than 5 seconds. Do you know that there are some behavioral limitations of dict that arise from a specific optimization in the implementation in C of dictionary iterators? If you create a new python following those documents, it is possible that you will allow a perfectly reasonable behavior that would fail in most other python interpreters.

> Well, even for the section "names" it just forgets to say if imported and non-imported names all share the same encoding and which should it be - just a nitpick, but with less than 5 seconds

https://www.python.org/dev/peps/pep-0263/

Names aren't unique.

> Do you know that there are some behavioral limitations of dict that arise from a specific optimization in the implementation in C of dictionary iterators?

I'm rather curious what you're referring to here, do you mean dict-ordering, or something else?

Sorry, but "names aren't unique" does not even begin to define uniqueness - "from ... import X" imports and X; great; should it replace an "X" in a different encoding in the local namespace, or not?

I can tell you it has to do with iterators, and maybe someone will comment on what that is.

I mean... I had not even yet heard the talk that others have pointed you to (from Armin Ronacher); after having gone several times down the rabbit hole of looking at what the interpreter is doing in specific scenarios (and I like lots of things, at the language level, that python does, the terseness and expresiveness that it brings) I also think that python is a very complex language under a soft-looking skin.

I follow Python since 1.6, and occasionally use it for portable scripting when on UNIX platforms (PowerShell on Win), and many aren't really aware that Python is Ada/C++ level of complexity, even if on the first contact seems like the new BASIC.

Besides the nuances of how everything is executed, there are occasionally breaking changes between minor language revisions.

You cannot just pick up a random Python script and be sure it still behaves the same way across all minor revisions.

By names aren't unique, I mean with respect to "encoding", everything is the same. It seems like you're using "encoding" to mean something it doesn't? Do you just mean like "value"?

> I can tell you it has to do with iterators, and maybe someone will comment on what that is.

This sounds like you don't know what it is.

> By names aren't unique, I mean with respect to "encoding", everything is the same. It seems like you're using "encoding" to mean something it doesn't? Do you just mean like "value"?

I think the GP means character encodings.

So the intent here is to ask whether (for example) a foo defined in a ISO 8859-1 encoded file is overidden by a foo imported from a Windows-1256 encoded file.

> I think the GP means character encodings.

Then the link I posted answers their question. Names aren't unique in how encodings are handled. Files are decoded and canonicalized as a unicode string. If the identifiers are the same after canonicalization, then yes they are equivalent. If they aren't, then they aren't.

Ah, I misunderstood what you meant by "aren't unique". I would have phrased that as "names aren't treated differently", or something similar.

My gut instinct is that many of Python's quirks are the reason for it's popularity. Though I might not be understanding your suggestion. Could you give a specific example of something you would clean up if you were able to? I have the video in a tab but won't be able to watch until later.

I think "a + b" is a good example.

I really recommend the talk I linked (https://youtu.be/qCGofLIzX6g), it gets deep into this stuff. I don't think anyone benefits from "a + b" having so many special cases.