Stabilize having the concept of "validity invariant" and "safety invariant"? Under which name?

[RalfJung]

It's been more than six years since my blog post that introduced these terms, and I think it is clear at this point that the concept of these two kinds of invariants is here to stay. We should start using this concept in stable docs, so that we can write clear docs.

The main thing that gives me halt here is that I am not happy with the terminology. Personally I regret calling them "validity invariant" and "safety invariant"; I now think that "language invariant" and "library invariant" are better terms. They go along nicely with the terms "language UB" and "library UB" that we have also been using already. I don't feel comfortable pushing for using these terms in stable docs until we have this resolved. We had #95 open for a while to find better terms, but that got closed as part of our backlog cleanup.

@digama0 was also recently confused by the fact that we call these "invariant" when they are not strictly speaking invariants that hold on every step of execution -- they are more invariants that hold about values at given points in the program. In verification we also talk e.g. about "loop invariants" that only hold at the beginning (or some other fixed point) during each loop, not all the time during the loop, and at least in Iris our "invariants" can be temporarily broken while they are being "opened" (and closed again within the same atomic step). The work on the anti-frame rule also uses the term "invariant" for things that are true between the operations on a data structure, but not during an operation. So IMO it is justified to use the term "invariant".

@rust-lang/opsem I'd like to commit to using the terms "language invariant" and "library invariant", and then start using those in the reference and stable docs. What do you think?

[joshlf]

Another angle to consider: Once we settle on agreed-upon terms and definitions and make them official, how do we make it clear in existing documentation whether we're using terms in their old or colloquial meaning or whether we're using them according to these new definitions?

I propose that we include a rule (that will live alongside the definitions of these terms) that prose must only be considered to be using these terms precisely when it links to the definitions. Consider the following text:

It is a safety invariant that a bool value always has the bit pattern 0x00 or 0x01

It is a safety invariant that a bool value always has the bit pattern 0x00 or 0x01

The former text would be considered to be using "safety invariant" in an imprecise sense, while the latter would be considered to be using it in a precise sense (consistent with whatever docs that link points to).

This should allow us to incrementally migrate existing documentation while leaving it unambiguous whether a given set of documentation has been updated. It will also act as a forcing function to ensure that documentation authors are precise in their language (which has been a problem historically since there hasn't been clear agreement on the meaning of terms).

[RalfJung]

Current docs shouldn't be using this term at all, so I don't think that question is related to this issue. I agree in general that we should treat defined terms in some systematic way, but that's a much broader discussion and off-topic here.

[arielb1]

@rust-lang/opsem I'd like to commit to using the terms "language invariant" and "library invariant", and then start using those in the reference and stable docs. What do you think?

I don't like these. Many library invariants are not safety invariants (e.g., if you have a non-deterministic Hash function, you are very likely to not find your items in an HashMap, but nothing unsafe will happen), and some language invariants are safety invariants (e.g., if you have aliasing &mut references, then as long as you don't use them nothing bad will happen).

So there's at least:

1. abstract machine invariant - if you violate this demons might fly out of your nose, immediately do not pass go, even if you would immediately afterward call _exit(0) without calling any intermediate library function.
2. library non-safety invariant - if you violate this, the library might do something safe but undesirable (e.g. a non-determinstic hash on an HashMap)
3. library "validity" invariant - if you violate this and call a library function on that object, you might have demons flying out of your nose. But if you don't call a library function on that object, nothing bad will happen. e.g. I believe non-UTF8 &str falls here.
4. safety invariants - if you violate this, you can write more or less carefully-crafted safe code that will violate an abstract machine invariant [but if you don't write that particular safe code, the program will do something very well-defined and possibly useful].
   4.1. including fully library safety invariants like an Rc with an invalid reference count - which should not cause UB as long as it doesn't unexpectedly reach 0.

I think that "safety invariant" is a good name, but "validity invariant" is not a particularly good name for "if you violate this demons will pop out of your nose". tho maybe "language invariant" is a good name (so language invariant/safety invariant).

[Lokathor]

I think any two names that do not share the first letter are better than two names that do share the same first letter.

So I vote for validity/safety over lang/library. But also any two other words of differing first letter would be fine too: lang and safety, for example.

[RalfJung]

Many library invariants are not safety invariants (e.g., if you have a non-deterministic Hash function, you are very likely to not find your items in an HashMap, but nothing unsafe will happen), and some language invariants are safety invariants (e.g., if you have aliasing &mut references, then as long as you don't use them nothing bad will happen).

Well, you've made your own choices here by calling these "library invariants" and "language invariants"; choices I would not agree with. ;)

So I vote for validity/safety over lang/library. But also any two other words of differing first letter would be fine too: lang and safety, for example.

So do you propose we also call it language UB and safety UB? That doesn't make a lot of sense, and IMO it'd be good to align those terms with the invariants that cause the respective UB when violated.

I don't recall us ever abbreviating validity/safety invariant with the first letters, so I don't think it's very important that they have different first letters.

[Lokathor]

But there isn't actually safety UB is there? All safety invariants are there because when violated they can allow otherwise fine code to end up breaking a language rule somewhere later. As far as I'm aware, there's just the one kind of UB.

[RalfJung]

Library UB is real and not the same as language UB. For instance, it is library UB to call any &str method with a non-UTF-8 str, but it is language UB only for some operations that happen to rely on the UTF-8 invariant in a way that triggers language UB (i.e., a Miri error) when the invariant is violated. Future library updates may change existing methods so that more (or fewer) of them have language UB when invoked with a non-UTF-8 str.

[zachs18]

As far as I'm aware, there's just the one kind of UB.

They go along nicely with the terms "language UB" and "library UB" that we have also been using already.

(From the OP)

The UB you are referring to is also called "language UB", and "library UB" is used in contrast to mean basically "a violation of library invariants/preconditions/etc that could lead to (language) UB depending on usage/library implementation details/etc", which is useful to have a succinct term for.

[digama0]

So do you propose we also call it language UB and safety UB? That doesn't make a lot of sense, and IMO it'd be good to align those terms with the invariants that cause the respective UB when violated.

I would call them "language UB" (or just UB as I think there is only one thing that should get that name) and "safety violation" respectively.

[Lokathor]

Yeah, see, I'm in agreement with @digama0. If you have a &str and unsafely set the bytes to not be utf8, then that could lead to UB, but it's not actually UB the moment the bytes are wrong.

I don't think we should call that state of having invalid bytes "library UB". I don't think we should call any other similar situations "library UB" either. I do like the term "safety violation".

Otherwise you have to start explaining to people that sometimes there's something called UB that they're allowed to do anyway, as long as they fix the situation before anything "really bad" happens. And that's a very easy thing for people to misunderstand, or only halfway remember months after the fact.

[RalfJung]

Violating such library preconditions is often called UB, and I think it makes sense. UB basically means "you violated the contract of this API and now all guarantees are void". Language UB is about the contract between the programmer and the compiler (where the "API" is the language itself); library UB is about the contract between the library author and the client author.

[Lokathor]

Right, except I'm telling you that what people often end up hearing is, "I'm allowed to do some types of UB".

I think that's bad, and if we're going to deliberately pick terms, we should deliberately pick terms that don't let people think that "sometimes UB is okay". Because that's a real thing people have said to me, and I've had to stop and explain to them what's "actually UB", and that they really can't do it, not even sneakily.

So call them lang invariants and lib invariants if you want, but i strongly suggest that you don't call them that if you want to draw a connection to "lang ub" and "lib ub", because those terms are not good terms that i have seen do harm to people's understanding of rust on multiple occasions over the years.

[RalfJung]

You're not allowed to do library UB with other people's libraries either. I have seen this analogy work pretty well, too, so I wouldn't be so quick to discard it.