I'm surprised the Unsafe Code Guidelines Working Group hasn't been mentioned in this thread yet. It's a work in progress, but they are hashing out what is and isn't undefined behavior (UB), what contracts must be honored at safe/unsafe boundaries and within unsafe blocks generally, etc.
For example, they've documented a distinction between validity invariants and safety invariants. The distinction is relevant to the discussion about transitivity; if you violate a safety invariant such as putting non-utf8 values into a
String, for example, it may not immediately cause UB -- but it creates the possibility of safe code causing UB.
They call this library unsoundness:
[A] library (or an individual function) is sound if it is impossible for safe code to cause Undefined Behavior using its public API. Conversely, the library/function is unsound if safe code can cause Undefined Behavior.
The concept of
unsafe generally is that a program with no
unsafe is necessarily sound (has no UB). And a program with
unsafe where every
unsafe block maintains the proper invariants is also sound. (Formalizing the invariants is the work in progress.)