{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiauf5v6hbu5u7grzyq7d74nxpbdksp7wqs6y5k56im2ugshriokui",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mpibuijgsfi2"
  },
  "path": "/t/language-vision-regarding-safety-guarantees/24418#post_4",
  "publishedAt": "2026-06-30T03:43:14.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "Creusot",
    "flux",
    "TrustedLen",
    "verify the unsafe bits of the Rust stdlib"
  ],
  "textContent": "Evian-Zhang:\n\n> This means it is suggested that:\n>\n>\n>     pub fn safe_api<T: Ord>() {\n>         check_t_implement_ord_logic_contract_correctly()?;\n>         unsafe { use_ord_logic_contract_for_unsafe_operation(); }\n>     }\n>\n\nHow is `check_t_implement_ord_logic_contract_correctly()` is supposed to work?\n\nIt'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.\n\nBut 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`.\n\nBut 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!\n\nBut 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)\n\nWell 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)",
  "title": "Language vision regarding safety guarantees"
}