{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreigo5jxzs6isawee3imxf4vkbqixelfdnlm5m5zjlqnylydoyx3aji",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mpqsihxgdcq2"
  },
  "path": "/t/language-vision-regarding-safety-guarantees/24418?page=2#post_38",
  "publishedAt": "2026-07-03T13:41:33.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "[1]",
    "↩︎"
  ],
  "textContent": "What you describe is essentially the \"Rust Hypothesis\" (self-encapsulation: there are no safety guarantees). I also believed this was the convention before I learned that it was not the case and \"logic contracts are safety guarantees\". I believe this is a good signal that the language should probably take an official stance here.\n\nNote that while the Rust Hypothesis guarantees that \"safe code cannot cause UB outside its unit of implementation\", it is a bit extreme. It could be refined to authorize the scope of unsafe to leak to dependencies in a controlled way using safety guarantees, exactly like the scope of unsafe is allowed to leak to clients in a controlled way using safety requirements. You can still locally review code for safety (in particular with the `robust` keyword, which requires unsafe code to provide safety guarantees).\n\nais523:\n\n> I guess my main concern with your point of view is that I don't think \"a unit of implementation should be checked for soundness as a whole\" is acceptable in cases where the unit of implementation is too large.\n\nMaybe you missed the part where you get to choose what a unit of implementation is: crate, module, item, etc. I agree that the language should recommend that units of implementation with directly-unsafe code should not exceed 100 lines. In some case that's the crate, in others that's the module, and in the worst case that's the function.\n\nais523:\n\n> In a way, the promise of Rust is \"to prevent a particular class of bugs – those that compromise memory safety – you only have to review `unsafe` blocks and the code they depend on\".\n\nIndeed, that's the current promise. More precisely: to prevent safety bugs, you only need to review unsafe code[1] and the code it depends on. The problem is that that last part is unbounded, and in particular may escape the unit of implementation. So you simply can't review it without pinning those dependencies (which has bad properties). And even with pinning, you may end up extending your unit of implementation beyond what is reasonable to review.\n\nais523:\n\n> (Or another way of looking at it: for unsafe code you need to be able to _prove_ the safety condition correct, and if it is too complicated, e.g. relying on the correctness of a large dependency, you can't do that.)\n\nThat's not completely correct. You can't review a small dependency either. You would need to pin it first to make it part of your unit of implementation.\n\nMaybe what you're saying with \"large dependency\" is not that \"some of its implementations (past, present, and future) are large\" but rather than \"its logic contract seems hard to implement correctly\". Maybe you could defined it as \"there are no correct implementations in less than 100 lines\". But then what happens if that dependency decides to write a large implementation for performance, and that implementation ends up being incorrect in a corner case? From their point of view it's just a logic bug. They never claimed to implement the logic contract in less than 100 lines. They never claimed their implementations can be used by unsafe code. Maybe they care more about performance than being correct in all possible corner cases (even unrealistic ones).\n\nA safety contract makes this kind of interaction clearer. A unit of implementation can tell which parts of its API it will prioritize for being absolutely correct, by writing those property as safety contract, and which parts it will prioritize for performance (being possibly incorrect in rare cases), by writing those property as logic contract. I talk about performance but it could be anything else that could trump absolute correctness. As a client of such a unit of implementation, you don't need to guess whether that dependency is able to implement its logic contract correctly, you just assume its safety contract and they will get the CVE if they are incorrect. Also when they get reviewed for safety, those claims will be checked. There's no mixing between logic and safety.\n\n* * *\n\n  1. I guess that's what you meant, because unsafe impl and unsafe attributes matter ↩︎\n\n\n",
  "title": "Language vision regarding safety guarantees"
}