Language vision regarding safety guarantees

ais523:

The whole BTreeMap implementation seems to have been written using a principle of "let's not care about soundness requirements for our own use internally, and just mark the public APIs as safe or unsafe according to whether use from outside the module would be safe or unsafe", but this means that it isn't benefiting from the Rust compiler helping to catch soundness issues, and thus allows bugs like that to sneak through.

This is perfectly fine and just a matter of style. This is why I wrote that the concept of unit of implementation is subjective. Within a unit of implementation, there are no contracts (see below for nested contracts). The contracts are at the boundaries of the unit of implementation. And you prove that this unit of implementation is correct with respect to those contracts.

The maximum unit of implementation is the union of a crate with all its pinned dependencies recursively. In large projects like the standard library, it makes sense to consider smaller units of implementation like modules, since it would be too costly to review all of the standard library for correctness when changing arbitrary small and isolated parts. One could obviously push this even further (in particular for large modules) and consider every item (like function definitions) as units of implementation.

Since units of implementation have a natural nesting behavior (a crate with its pinned dependencies is made of crates, which are made of modules, which are made of items), there is naturally a notion of "nested contracts". In particular, an item has an "item-level" contract (its contract when seen as a unit of implementation), but it also has a "module-level" contract (the part of its module contract when that module is seen as a unit of implementation) if it's an item exposed outside the module, and similarly for its "crate-level" contract if it's an item exposed outside the crate. Contracts can always be rewritten into equivalent contracts, such that nested contracts imply the contracts their nested in (item-level implies module-level which implies crate-level). This is a "contract implication" so variance needs to be taken into account between requirements and guarantees.

In the case of insert_before_unchecked, there's at least 2 contracts: the one when seen from outside the standard library and the one when seen from inside. But there could be more depending on how the authors want to split the units of implementation. The problem as you noted, is that the unsafe keyword is unique, so it cannot necessarily match all contracts. The contract it must match is the highest-level contract (highest in the sense of most public, so crate-level for public items). So it's possible that an internally safe function (no safety requirements when used within the module) is marked unsafe because it's publicly unsafe.