Adapting the C++ standard, it could look like this:

• implementation-defined behavior: behavior for a well-formed program that depends on the implementation and that each implementation documents

  • note: the reference often delineates the range of possible behaviors.

• unspecified behavior: behavior for a well-formed program that depends on the implementation

  • note: implementations are not required to document the behavior.
  • note: the reference often delineates the range of possible behaviors.

• implementation-independent behavior: behavior for a well-formed program that does not depend on the implementation

  • note: the language reference explicitly documents the behavior.

These refer to well-formed programs. We might want to define that term as well:

• well-formed program: A Rust program constructed from Rust syntax and grammar rules that is well-typed.

  • note: in practice, a program that compiles successfully
  • note: well-formed programs might have implementation-defined, unspecified, or undefined behavior.

• ill-formed program: A Rust program that is not well-formed.

implementation-independent behavior: behavior for a well-formed program that depends on the implementation

This sounds strange to me. Shouldn't it be “that does not depend on concrete implementation”?

Yeah that should probably say "that does not depend on" instead of "that depends on"

Thanks, fixed.

I would prefer if we could make those definitions directly refer to behavior of the Rust Abstract Machine. That machine is the "core artifact" defined by the spec, after all.

For example, implementation-defined behavior would be aspects of the Rust Abstract Machine that are left open by the standard, but have to be specified precisely by an implementation. You say "the reference often delineates the range of possible behaviors", but isn't that "always"? Because without bounding the range of possible behavior, implementations could say "this is UB", and that does not seem very helpful?

Also, I think this should touch on the matter of stability. Like, I assume unspecified behavior is allowed to change from version to version of an implementation, but changing implementation-defined behavior is a breaking change?

That doesn't really apply to he "well-formed" part -- TBH that's nitpicking I care little about, other than one question: you are still implicitly using the term "a Rust program" without defining it. If you go down this route, please go all the way. ;)

I think we should always delineate the behavior, at least to say that it
cannot be defined to be undefined

Note that behavior could then still be "it resets the state of the Rust Abstract Machine to be empty". So, it seems we need a more specific parameterization, that well depend on the individual case.

In the context of what I discussed with @rkruppe in the other thread, it seems like we might also have "unspecified behavior" where we can't really say what happens though, such as messing with page tables. Not sure where to fit that in. Some of this related to whether it is even possible to think in terms of the Rust Abstract Machine -- which leads us into a cycle, because it is the Rust Abstract Machine that defines whether it is even possible to think in terms of hardware or page tables...

• unspecified: the implementation doesn't have to say what the behavior is

The main purpose of unspec as I see it is to facilitate future language design by giving it options to work with. As such, what I really want from unspec is:

unspecified: The implementation may not guarantee what the behavior is.

(...other than to document it for internal purposes.)

@RalfJung agreed. FWIW I think it would be ok to start with a loose definitions of these terms, and making them precise over time. Initially it would be enough for me if the definitions were not contradictory. E.g. if we define undefined behavior as "behavior for which the abstract machine provides no guarantees", then the "unspecified behavior" definition proposed by @Centril might be undefined behavior. We don't want, e.g., the optimizer reasoning that if your program exhibits unspecified behavior that state is unreachable (as opposed to UB, where that would be fine).

A PR to define these terms (unspecified vs implementation-defined) would be very welcome.