Language vision regarding safety guarantees

Evian-Zhang:

This means it is suggested that:

pub fn safe_api<T: Ord>() {
    check_t_implement_ord_logic_contract_correctly()?;
    unsafe { use_ord_logic_contract_for_unsafe_operation(); }
}

How is check_t_implement_ord_logic_contract_correctly() is supposed to work?

It's making a check at runtime, but we need a check at compile time. Probably using something like Creusot or flux (or the many other verification frameworks - not sure why there are so many), if they can verify contracts in traits, and give a proof of correctness. Since most people don't do that, the BTreeMap must not cause UB even if the Ord impl of the type of the key has bugs.

But if we had a proof of correctness of some code, we could rely on it for soundness. If we don't, we must manually inspect the code and personally assess whether it is correct. The unsafe { } block is a way of signaling you did all the work (including auditing all and every safe code you rely upon). That's the price of unsafe.

But we can't normally rely on the correctness of generic safe code, because we can't, at the point we wrote unsafe { }, verify all impls (unless it's a sealed trait), since it's unbounded. In particular we can't ever rely on the correctness of downstream safe code!

But the Rust solution of such unsafe problems is more unsafe. If we make a trait unsafe trait TrustedOrd: Ord { } with no methods, anyone that write unsafe impl TrustedOrd for MyType is signaling that they are asserting that specifically the Ord impl of MyType can be trusted by unsafe code. This is not particularly great because this is still not verified by the compiler - we need a someone to personally vouch for this impl. (Note, that's how TrustedLen in iterators work)

Well there is a better approach now that we have some verification tools. We can write a contract in, say, Creusot, and as long as we run the checks at compile time we can verify that some safe code is correct. Or, even better, verify that some unsafe code is correct! (and won't cause UB). Right now there's a project to verify the unsafe bits of the Rust stdlib (which is weaker than full verification of the stdlib APIs - which is what we need, since we generally trust that the stdlib is correct in most unsafe code)