Unbounded implementation specific behavior.

(Warning: this issue could be too pedantic, I'm not sure, please let me know if it appears that way, but I don't think that it is.)

It seems to me that (according to the specification) anybody can declare anything to be a conforming dart implementation by declaring all violations to be "implementation specific behavior"?

Consider this comment (and issue) for context, quote:

In any case, each language processing tool (compilers, the analyzer, ...) has a number of implementation specific behaviors, and they are intentionally not mentioned in these specification documents [...].

and

Each tool is allowed to do whatever it wants when it comes to implementation specific behavior

If the specification doesn't limit the scope of what it considers to be "implementation specific behavior", wouldn't this trivialize the act of developing a conforming implementation by giving implementers the freedom to call any violation of the specification "implementation specific behavior" which would turn everything in the specification into a recommendation?

That is, one could call the following program written in dart a conforming dart implementation:

dynamic novaDart(String code) => null;

"But it doesn't compute anything useful!?" "Well, that's correct, this change in behavior is implementation specific behavior!"

ECMAScript seems to prevent this by stating the following: A conforming implementation of ECMAScript must not redefine any facilities that are not implementation-defined, implementation-approximated, or host-defined.

It seems to me that (according to the specification) anybody can declare anything to be a conforming dart implementation by declaring all violations to be "implementation specific behavior"?

I disagree with that characterization. A conforming Dart implementation must implement at least one Dart language versions correctly, which means:

Correctly parsing all grammatically correct inputs, per the grammar of that version of the Dart language specification.
Correctly applying the static semantics to that program per that version of the Dart language specification, and not rejecting an otherwise correct program.
Generating an output which, which run, correctly implements the runtime semantics of the program per that version of the Dart language specification.

There is a "turtles all the way down" issue here because the language specification doesn't specify what the platform library functions do. Let's assume that they actually do what their documentation say. That should ensure that invoking the print function has an externally visible effect, so we can't just compile the entire program away and claim that it "did what the semantics say", without any extrinsic effect.

Where tools have some leeway, is that they can allow more than the language specifies. They can provide implementations for external declarations. They can provide implementations for entire under-defined classes, like dart:ffi does. Those are platform specific extensions to the language. And they can provide platform specific libraries too, like dart:io. That's not restricted by the language specification. If you don't use those extensions, and just write pure Dart, the tools should treat that correctly.

And then there are parts of the specification where specific behavior is left "implementation specific". It's usually not completely undefined, just an option between different valid choices. I think the most unspecified part is the ordering of asynchronous tasks.

So while each tool can have its own implementation specific extra features, they cannot just ignore the language specification with impunity. The user must, somehow, ask for exceptions, and if they do not, the language specification must be applied to the Dart code.

Where tools have some leeway, is that they can allow more than the language specifies.

My argument is that not limiting the more is the issue here.

Allow me to be a little bit more explicit in my reasoning.

If I assume the spec to be a proxy for a formal system that allows me to reason about Dart code, then I expect that this system is sound (everything that the spec states about Dart code is always true) and complete (everything that's needed to derive anything about Dart code is inside of the spec).

If somebody were to translate the specification written in natural language into some less expressive (but a sufficiently expressive and more precise) system, such as one based on intentional programming, or a language workbench such as Spoofax or MPS, then a situation would come up where "implementation specific behavior" would need to be precisely specified.

type ImplementationSpecificBehavior {}

variant ThingsRelatedToExternalDeclarations is ImplementationSpecificBehavior {}

variant ThingsRelatedToFFI is ImplementationSpecificBehavior {}

// ... other ImplementationSpecificBehavior that the spec is explicit about

But if the spec does not "seal" the ImplementationSpecificBehavior type, then my argument is that, the spec can be complete, but nothing else must hold because users are free to add new variants to ImplementationSpecificBehavior:

variant AllViolationsAreImplementationSpecificBehavior is ImplementationSpecificBehavior {}

So to me, this seems like a "hole" in the formal system that the spec represents. And ECMAScript explicitly fixes this "hole" by "sealing" ImplementationSpecificBehavior by saying that everything that is not explicitly specified as ImplementationSpecificBehavior can't be changed.

I agree with @lrhn about the fundamental perspective on this question: "Is implementation specific behavior an unlimited loophole?", and my answer is, in short, "No, a specified behavior cannot be considered implementation specific".

For example, int i = 'Hello'; must be reported as a compile-time error (assuming that int resolves to the declaration in 'dart:core'), and a compiler that doesn't report this error (and compiles it as, say, int i = 'Hello' as dynamic; or int i = 0;) is not a conforming implementation of Dart.

It is true that there is nothing in the specification that prevents a compiler from sending a copy by email of every library that it encounters, or colorizing its error messages, or causing the nearest power plant to stop delivering power to anyone whose house number is even. I think it's fair to say that it would be difficult, and unnecessary, to close every loophole in this sense (and we might even want the colorized error messages ;-).

Even in the case where we are considering a specification which is a Coq implementation of every Dart tool along with a lot of proofs (termination of type checking, type soundness at run time, whatever), I still think the problem remains: If we assume that this strictly verified formal artifact exists, every (other) implementation of Dart would still have basically all the same loopholes.

I don't think this is a particularly big problem. We do operate in a world where lots and lots and lots of things will only work because so many actors approach the role they are playing in good faith, and they might even notice loopholes without exploiting them.

With that, I'd suggest that we settle this discussion by seeking an answer to the following question: Does the language specification need to change in order to maintain that specified behavior isn't implementation specific?

Erik wrote:

I think it's fair to say that it would be difficult, and unnecessary, to close every loophole in this sense

This feels like a similar argument that some people make against static type systems "well, they can't protect you from all errors, so why have them in the first place?" I think you would agree that having some restrictions (even if they can't be "complete" and capture everything) is useful. Laws don't capture everything and that's why case law exists. The static type system of Dart can't "prove" everything, but it is still useful. If you are saying that the spec shouldn't attempt to close loopholes (If we assume that this is one) because we can't guarantee that all loopholes are closed, then I would strongly disagree with that.

I believe that the spec should be as restrictive as possible. (e.g. all implementation specific behavior is non-conforming) and make an attempt (in an allowlist-style-manner) to open up "hooks" for implementations to inject their implementation specific behavior into.

This opinion seems to be mirrored by, as mentioned, the ECMAScript spec:

The ECMAScript spec says:

A conforming implementation of ECMAScript must not redefine any facilities that are not implementation-defined, implementation-approximated, or host-defined.

Furthermore, the C++ standard seems to contain a similar statement:

Working Draft, Standard for Programming Language C++ says:

A conforming implementation may have extensions (including additional library functions), provided they do not alter the behavior of any well-formed program.

And the C Standard is even more explicit about what well-formed means:

The C Standard says:

A conforming implementation may have extensions (including additional library functions), provided they do not alter the behavior of any strictly conforming program. A strictly conforming program shall use only those features of the language and library specified in this International Standard. It shall not produce output dependent on any unspecified, undefined, or implementation-defined behavior, and shall not exceed any minimum implementation limit.

I believe to have established that it is not uncommon to attempt to close such loopholes. Can this be useful in any practical way? Yes. What follows is evidence for that:

Erik wrote:

Even in the case where we are considering a specification which is a Coq implementation of every Dart tool along with a lot of proofs (termination of type checking, type soundness at run time, whatever), I still think the problem remains: If we assume that this strictly verified formal artifact exists, every (other) implementation of Dart would still have basically all the same loopholes.

If there are no loopholes because the Dart spec claims those loopholes to be non-conforming, then all these other implementations would simply be non-conforming. Would there be an issue with that?

Furthermore, this seems to assume that there is no way to use formal proofs to synthesize a correct implementation. Consider the compcert C compiler. Quote:

The CompCert distribution by AbsInt says:

The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.

A quote from: Finding and Understanding Bugs in C Compilers

The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.

The Dart ecosystem is, in some ways, more complex than the C ecosystem. For example, it has a JIT. There are ongoing research efforts by at least one person to synthesize efficient JIT compilers. Quote:

Building a baseline JIT for Lua automatically says:

[...] we used Deegen to automatically generate the fastest Lua 5.1 interpreter to date, outperforming LuaJIT’s interpreter by an average of 34% across a variety of Lua benchmarks.

I believe to have shown that:

it is not uncommon to attempt to close such loopholes
closing any loopholes can aid in the development of synthesized tooling that is guaranteed to be correct
synthesized tooling can beat handwritten implementations when it comes to performance.

Performance and correctness are all properties that "Dart" seems to care about. Therefore, I believe that being more restrictive (or at least explicit) about any potential loopholes is important and that the Dart spec should aim to do that.

This feels like a similar argument that some people make against static type systems

I don't agree on this: I'm saying that specified behavior is not implementation specific behavior, and hence we have a notion of what it means to be a conforming implementation for a Dart analyzer or compiler which is vastly less permissive than "do whatever you want". In particular, they must exhibit the specified behavior.

When I say that it is

difficult, and unnecessary, to close every loophole

I'm referring to the specification of the set of behaviors that may be classified as implementation specific.

For instance, if we wish to allow colorization of diagnostic messages then we would have to specify that the colors of diagnostic messages is an implementation specific behavior; this implies that the colors we see all the time when using dart and dart analyze are allowed for a conforming implementation.

Also, the notation used to indicate the location of code in a library is implementation specific behavior; so <line number> ':' <column number> is OK. Similarly for the notation that specifies the library itself.

What I'm saying is that there is no end to the amount of detail that we would have to specify if we were to embark on the adventure of specifying which kinds of behaviors are implementation specific, rather than just saying that it is every behavior which isn't specified behavior.

On the other hand, if we do settle on the definition that implementation specific behavior is any behavior which isn't specified behavior, and we allow implementation specific behaviors, then we do have loopholes: We do not specify that it is a non-conforming behavior for a Dart compiler to format your harddisk, or use white characters on a white background to print certain error messages, etc.

That's the point where I prefer to rely on trust: Those implementations are not violating the specification, but they are also not likely to remain in the marketplace for very long.

All in all, I think this state of affairs is useful: We have a notion of specified behavior, tools need to have those behaviors in order to be conforming implementations of a Dart analyzer or compiler (or any other Dart language processing tool), and every behavior which is not in the topic area of the language specification documents is chosen by the maintainers of the tools.

It's more like saying "Let's have a static type system. It works like this: [detail, detail, detail]. With respect to cases where the type system does not have an opinion, go ahead. For example, you can write 1 ~/ 0 in your program, and it's not going to be an error according to the type system. We do not wish to enumerate all the wrong programs that aren't type errors."

Of course, the discussion about specification conformance is dealing with language tools, and the type system example is dealing with programs, so you have to compare two discussions with different levels. That's the reason why the first discussion is talking about "which implementations of a Dart compiler/analyzer are specification conforming?" and the second discussion is talking about "which programs are accepted by a compiler/analyzer?".

A conforming implementation of ECMAScript must not redefine any facilities that are not implementation-defined, implementation-approximated, or host-defined.

This is exactly what I'm saying we have with Dart: You cannot claim that an implementation of a Dart compiler or analyzer is conforming to the specification unless it exhibits the specified behavior.

ECMAScript has more than one category of "other" behavior: implementation-defined, implementation-approximated, and host-defined. Dart could define as many buckets of "other" behavior as we want, but it doesn't change the meaning: Anything which is in one of those "other" buckets is up to the given toolchain (or, with ECMAScript: the given host).

About C++:

A conforming implementation may have extensions (including additional library functions), provided they do not alter the behavior of any well-formed program.

I see a bit less than 4 pages of index entries referring to specific locations in the given C++ international standard document where a specific behavior is classified as implementation specific.

This corresponds to the implementation specific parts of Dart that we have specified: Assertion checking (how to enable/disable it); the binding of an external function declaration to an actual foreign function; the use/non-use of an implicitly induced forwarding method in connection with certain dynamic type checks of covariant function parameters; the errors that may occur during actual loading of a deferred library; the interpretation of a URI as a reference to a disk file (or some other entity).

We won't be able to fill almost 4 pages of index references with that, but this is also because (apparently) most of the C++ topics in this index are concerned with standard library functions.

In any case, I don't see any rules about colorization of error messages in this specification document (searching for 'color' only brings up enum related examples), so perhaps C++ has a loophole there, too?

And nothing about erasing my harddisk, either? I don't immediately know how to check that, but if you can find language in this C++ specification saying that this cannot occur with a standards conforming C++ compiler then please give us a pointer to the relevant text.

About C:

A strictly conforming program shall use only those features of the language and library specified in this International Standard.

We don't have the notion of "a strictly conforming program", but the relevant concept is "a program", with the understanding that it is a Dart library, plus a set of libraries and parts that are reachable from there using imports and part-of directives, and none of them have a compile-time error.

That won't suffice for a C program because there is no way for a C compiler to detect certain violations: The effect of invoking a function with actual arguments whose evaluation order matters is undefined behavior (like g(f(1), f(2)) where the execution of f() has some side effects).

Again, I don't see any reason to claim that C has fewer loopholes than Dart. It actually has a lot more, because you can't know what g(f(1), f(2)) will do at run time, and it could indeed erase your harddisk. Dart specifies that the evaluation of actual arguments occurs in textual order, and hence the side effects are specified just as precisely as they are for g(f(1)).

I believe to have established that it is not uncommon to attempt to close such loopholes.

I haven't seen anything that goes beyond 'specified behavior isn't implementation specific behavior'.

About CompCert: They don't even mention the behavior of the language processing tools apart from the properties of generated code.

It would be a very interesting experiment to build a Coq implementation of the Dart tools, and prove that they generate code that satisfies certain properties, e.g., that the generated code maintains heap soundness, based on some assumptions about about the nature of the hardware (e.g., there will not be any fast particles from outer space changing the value of a storage cell, and stuff like that).

it is not uncommon to attempt to close such loopholes

I haven't seen any examples in the specification of those other languages, they are all inside the boundaries of what we already require by saying that 'specified behavior isn't implementation-specific behavior'.

closing any loopholes can aid in the development of synthesized tooling that is guaranteed to be correct

Certainly! But that would probably target specification language ambiguities, that is, topics where the specification documents do not describe the specified behavior in sufficient detail.

Of course, we could also try to specify that the compiler must not print light yellow error messages. But there is no end to the set of things that a compiler/analyzer shouldn't do, and which is at the same time not covered by the specification documents, and I think we should just acknowledge this as a fact of life.

synthesized tooling can beat handwritten implementations when it comes to performance.

Perhaps. Also, they might be more correct than hand-written ones, especially if the process whereby they are produced from a formal artifact like an executable specification is less complex than creating the compiler by hand. However, they are also likely to beat handwritten implementations in terms of development time: Writing that Coq model first will take extra time.

The Coq model is cool, but we aren't going to get it for free. ;-)

they must exhibit the specified behavior [...] This is exactly what I'm saying we have with Dart: You cannot claim that an implementation of a Dart compiler or analyzer is conforming to the specification unless it exhibits the specified behavior.

Can you clarify whether you think that the Dart specification explicitly says that, or are you saying that that is specified implicitly by assuming good faith?

I don't see any rules about colorization of error messages in this specification document (searching for 'color' only brings up enum related examples)

I don't think that pure colorization of output messages is a useful example for discussing the issue that I'm trying to get at, but, for example, if an implementation would attempt to solve an unsolvable problem before choosing a color (and so no choice would ever be made), then It looks to me like the other specifications are pretty clear that that would not be a conforming implementation because terminating programs executed in such an implementation would not terminate anymore and so that implementation would have changed the behavior of well-formed programs.

Consider this part from one of the examples that I provided that you quoted:

[...] extensions [...], provided they do not alter the behavior of any well-formed program

Wouldn't this explicitly prevent implementations from providing a print function like this?

void print(String value) {
  for (;;) {}
  stdout.print(value);
}

I agree that the current state of affairs is useful.

I agree that maybe the other specifications are not complete in capturing all possible unwanted behaviors (like the examples that you gave about coloring output or erasing harddisks) and so it wouldn't necessarily make much sense to try to do that just for the sake of doing that.

My primary concerns are the following:

I think it would be good if the "domain of discourse" for what the specification considers to be implementation specific behavior is finite/sealed/closed. (even if each "entity" of that "domain of discourse" makes few restrictions)

I think that each "entity" of the "domain of discourse" of implementation specific behaviors could guarantee certain useful properties without being too restrictive.

Two important properties that I would consider useful (and not too restricting) are termination and referential transparency.

I see no reason why, for example, a print function should ever be allowed not to terminate or have side effects. The same can be applied to other core APIs such as String/double/num/int.

Once we are explicit about referential transparency we could go further and be explicit about algebraic properties such as that BigInt.one and BigInt.* or "" and String.+ form a monoid. (Is this useful? I think yes, compilers could use some general purpose system to make use of such richer algebraic guarantees).

A different example that I would like to give (that is not related to APIs) is with respect to system libraries and the fact that they can extend syntax (which we have established in https://github.com/dart-lang/sdk/issues/52594).

The current spec assumes PEGs for its grammar snippets. I believe that PEGs are known to go beyond CFGs in terms of expressivity. To the best of my knowledge, important problems such as efficient, incremental and error-recoverable parsing have not yet been successfully solved (or proven in practice) for PEGs, but this is a problem that is more or less solved for CFGs (and proven in practice by tree-sitter). It looks to me that, in practice, the spec has little authority over the parsing theory required to parse Dart because it allows implementations to ship code that looks like Dart code, acts like Dart code, participates in tools as Dart code, but isn't Dart code only according to the spec.

I think the specification could be more restrictive here as well. But I think this deserves its own issue, I'm not going to go deeper into it here. I'm just mentioning this to provide an example of a different place where I think it would be useful for the spec to be more restrictive because it would guarantee that Dart can be parsed efficiently, incrementally and in a way that provides excellent error messages (all at the same time).

To summarize, I am not trying to say that what the current spec specifies is wrong. I just believe that we can be more restrictive without sacrificing much, and that we could gain a lot by doing that.

And to be clear, I'm not necessarily asking for anything to be done just yet. I just want to make sure that we are on ships that steer into a more or less common direction.

Edit: I removed a minor incorrect example.

The Dart language specification does not try to specify everything in the platform libraries.

It mentiones a few libraries, types and members by name, and a compatible implementation of Dart should have those types in those libraries with those members. But, for example, the print function of dart:core is never mentioned in the language specification in normative text, only in examples.

The platform libraries are part of the Dart SDK, not the Dart language. There is no formal specification of the libraries of the Dart SDK, other than their own declarations and documentation. There is no attempt, or intent, to do a formal specification. And we do allow ourselves to make breaking changes to those platform libraries (very carefully, and preferably language versioned). We do not have library versioning (sadly, and "yet!").

That also leads us to a situation where asynchrony is part of the language, defined in terms of operations on instances of Future and Stream, and microtasks are mentioned in the specification, but not actually defined. (They are apparently sequential, since we can talk about a "later microtask", but the language specification itself doesn't mention the event loop otherwise, at all.)

The same with garbage collection. It's possibly mentioned in the specification, but not defined or guaranteed. We now have platform library features which say more about garbage collection than the language. And that's fine, because that is really part of the runtime environment, and not something inherent to the language. The language doesn't need to know what happens to object that can no longer be referenced, it only needs to say what happens if they are referenced. That's the entire point of garbage collection.

dart-lang / language

Unbounded implementation specific behavior. #3124