5 ms·

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

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/executionmodel.html https://docs.python.org/3/reference/datamodel.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.

chrisseaton 5y ago
> 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?
- aw1621107 5y ago
  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?
  - chrisseaton 5y ago
    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.
    - fcurts 5y ago
      > 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 (!).
      - chrisseaton 5y ago
        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-popl.pdf https://fsl.cs.illinois.edu/publications/bogdanas-rosu-2015-...
        fcurts 5y ago
        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.
  - c-cube 5y ago
    Standard ML certainly has clear specifications and proofs of soundness of the type system.
- nevermore 5y ago
  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.
  - chrisseaton 5y ago
    >> 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.__bool__ 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.
    - joshuamorton 5y ago
      > 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.__ 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 5y ago

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

aw1621107 5y ago
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?
- chrisseaton 5y ago
  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.
  - fcurts 5y ago
    > 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 (!).
    - chrisseaton 5y ago
      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-popl.pdf https://fsl.cs.illinois.edu/publications/bogdanas-rosu-2015-...
      - fcurts 5y ago
        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.
- c-cube 5y ago
  Standard ML certainly has clear specifications and proofs of soundness of the type system.
nevermore 5y ago
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.
- chrisseaton 5y ago
  >> 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.__bool__ 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.
  - joshuamorton 5y ago
    > 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.__ 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.