joshlf
commented
1 day ago 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
boolvalue always has the bit pattern0x00or0x01It is a safety invariant that a
boolvalue always has the bit pattern0x00or0x01
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
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 https://github.com/rust-lang/unsafe-code-guidelines/issues/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?