|
|
|
|
|
|
by chrisseaton
1679 days 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.__... - '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. |
|
|
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.