Language vision regarding safety guarantees

Possibly related to all this: part of the reason I was concerned about all the unsafe in BTreeMap is that it makes it harder to prove it to be sound, and I just came across a bug report demonstrating that BTreeMap does actually double-free with some Ord implementations. (In this case, the incorrect assumption made by Node is that Ord does not panic. an assumption that is wrong even for some standard library types like RefCell<u32>.)

I think the confusion about what unsafe actually means with respect to something like BTreeMap is probably responsible for this. The problem is that Root::split_off, which does not have any stated safety requirements, calls move_suffix, which also does not have any stated safety requirements, but move_suffix actually cause the BTreeMap to get into an invalid state (one in which consuming-iterating over it will cause a double free). This can cause unsoundness in safe code because Root::split_off continues by calling a user-provided trait method (which could panic, and then surrounding code could catch the panic in order to iterate over the invalid-state BTreeMap), but I would put the blame here on move_suffix for not being marked unsafe. (Suspiciously, move_suffix has a large unsafe block with no safety comment above it – but I think that isn't the problem that causes the unsoundness, rather the unsoundness is caused by the fact that it breaks invariants and does not document that it does so.)

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. I would have hoped for better from the standard library (i.e. using only a minimum of unsafe code that is carefully vetted to ensure soundness).