Language vision regarding safety guarantees

The talk of BTreeMap above got me interested: in theory BTreeMap should be implementable in safe code (by trusting the API of Vec, Box, etc.). So I was wondering what it was doing that needed the unsafe blocks.

I spotted three main uses of unsafe in BTreeMap's implementation. One of them was handling allocators (because it does the allocation and deallocation itself rather than relying on Vec or the like). This is probably because BTreeMap wants to be able to make multiple allocations, but store the allocator only once. This is a problem that should be fixable long-term (I have been working on scoped generics as a method of solving it), but it isn't fixed in current Rust, so unsafe it is. Fair enough.

The second is more interesting: BTreeMap internally works using a cursor API (which is accessible outside the module too, but unstable), and so it frequently uses cursor methods in order to do updates. As such, it is calling methods like btree_map::CursorMut::insert_before_unchecked, which adds a value to a specific point in a BTreeMap without checking that this is actually the right place in sorted order. The interesting thing about this method is that it's marked unsafe, even though abusing it shouldn't be able to cause undefined behaviour (only logic bugs): because BTreeMap is parameterised on Ord which is a safe trait, you could cause BTreeMap to insert values in the wrong place by making the Ord definition dependent on a global atomic variable, which you temporarily change just at the moment it tries to do the insertion (after the calling code has checked that the position is correct). As such, the unsafe here is basically just a lint rather than marking a potential memory safety issue (and in particular, if the code made any use of insert_before_unchecked's safety requirement for soundness, it would be unsound). It seems wrong to me to need an unsafe block in BTreeMap in order to call insert_before_unchecked, primarily because implementing BTreeMap entirely in safe code would be a sensible way to prove that it is memory-safe even in the face of broken Ord implementations, but the safety requirement on the function means that you have to use an unsafe block to call it and thus this proof is not available.

The third is caused by the Node type that the BTreeMap uses internally (implemented here). This uses an implementation technique that's very hard to implement in safe Rust, both because it tries to do a polymorphic recursion and because it's doubly-linked. This means both lots of unsafe internally, and also some unsafe within BTreeMap itself when it reborrows Nodes (because the way Node::reborrow_mut is defined means that the compiler can't check that the reborrow and original aren't used at the same time). I am wondering whether it would be worth rewriting Node to use more Rust-like data structures: in particular, the double-linking doesn't seem essential and may be counterproductive (it makes BTreeMap iterators /cursors O(1) rather than O(log n) size, but adds an O(n) overhead to the memory usage of BTreeMap and the allocations it references, which seems like a bad tradeoff to me. The polymorphic recursion does seem like it probably has a significant efficiency benefit, though.

It seems like an ideal safety vision would be able to easily prove that BTreeMap<T> is sound regardless of how broken T's Ord implementation is. For the Node-related unsafety, this is easy because Node<T> does not require T: Ord and thus (without specialisation) can't possibly do anything that would be broken by a malicious Ord implemetnation. For the allocator management, this likely shouldn't depend on the Ord implementation (the easiest way to prove this would be to write the code such that BTreeMap uses its allocator is used only with Node and never for any other purpose). insert_before_unchecked is an interesting case, though – I suspect the correct solution is something along the lines of "create an UnorderedBTreeMap that supports cursors, etc. but doesn't have any requirement on being ordered, then implement BTreeMap in terms of it using only safe code".