{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreibjcmhqplyrex44a7ml3jcaser2wohdfl5xqzllovduyw6fx6nvqq",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mpi34thrbja2"
  },
  "path": "/t/language-vision-regarding-safety-guarantees/24418#post_3",
  "publishedAt": "2026-06-30T03:34:10.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "@ia0"
  ],
  "textContent": "I also want to talk about my understanding about this problem.\n\n## Understand the contract\n\n\"Contract\" is a mature thing in programming, which includes \"requires\" and \"ensures\" that pre and post the target function. The ultimate goal of contract is to **modularize verification**.\n\nIn theory, for any executable, we can verify the correctness from entrypoint to end, sentence-by-sentence, entering every sub-function call, forking at every conditional branch. However, obviously, this is not practical.\n\nFunction-level contract saves the world: for a single function, we write contract of what it takes (\"requires\", or requirements), and what it returns (\"ensures\", or guarantees). The verification will be done to check whether \"requires\" + function body can derive \"ensures\". When encountering a sub-function call, it will not enter, but directly apply the \"requires\" and \"ensures\" of that sub-function.\n\nAfter understanding this, the \"safety-\" and \"logic-\" contracts are clear for \"requires\", as posted by @ia0 :\n\n> A public API defines (among other things) a **logic contract** (resp. **safety contract**) used to prove that programs execute their intended logic (resp. execute without undefined behavior).\n\nHowever, what does it mean for \"safety-\" / \"logic-\" contracts for \"ensures\"? One can never image how the downstream users use this function's output contract. In my point of view, **it is meaningless to talk about whether an \"ensures\" contract is for safety or for logic**.\n\n## Use the contract\n\nIn the old world of \"safe / unsafe\" without contract, the responsibility is clear: The caller of unsafe callee is responsible to make sure the \"Safety\" section of callee is meet in caller. If an UB is occurred:\n\n  * If the triggering condition is not described in \"Safety\" section of callee, then it's callee's fault\n  * If not, it's caller's fault\n\n\n\nHowever, the \"make sure\" part is not clear and more subjective. Rust has no mechanism to **check** whether the caller can make sure, which is for contract.\n\nIn the world of \"contract\", (if all related crates have well-written contracts), there is nothing subjective. The caller cannot \"claim\" to make sure, everything is verifiable. **A safe and verified code will never cause UB**.\n\nAnd if we want this to be true, then answer to the question 2/3 I posted above is that, **it's callee's responsibility to check every conditions that not covered in the \"ensures\" of upstream crate / std.** (Hopefully, Rust compiler could optimize those checks if they are trivial)\n\nSo in short, if we add contract to Rust, then the question about \"safe code never cause UB\" can be resolved by adding \"verified\" condition. And by verifying, there is no room for subjective and everything is verifiable.",
  "title": "Language vision regarding safety guarantees"
}