Language vision regarding safety guarantees

tczajka:

BTW, you seem to be confusing "using BTreeMap in your own unsafe code" vs "using unsafe APIs of BTreeMap". These are two separate choices. It's possible to use safe BTreeMap APIs in your own unsafe code.

I don't think I do. I'm exclusively talking about the first (since I'm only interested in safety properties of safe code in dependencies). But anyway, I think we agree overall, simply with different words.

Also thanks to your perspective there's a better candidate to what a fully explicit version of "safe code cannot cause UB" could mean (finally got the time to update the top post summary).