{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreihkvo36qtpa7kkbgrdedrexd7s4ooueaoy3dsiaeottwxg2uqm5ty",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mpibua267dw2"
  },
  "path": "/t/language-vision-regarding-safety-guarantees/24418#post_6",
  "publishedAt": "2026-06-30T04:36:22.000Z",
  "site": "https://internals.rust-lang.org",
  "textContent": "dlight:\n\n> It's making a check at runtime, but we need a check at compile time.\n\nSorry for the ambiguity in my post. Let's make things clear. Let's say you are author of library A, which has function `foo`. `foo` invokes `bar` in library B, and invokes unsafe function `baz` in library C. The safety requirement of `baz` comes from `bar`.\n\nWhat I propose is that:\n\n  * If author of library B writes verified contract of `bar`, and the \"ensures\" contract of `bar` contains the safety requirement of `baz`:\n\nThen author of library A does not need to do anything, just invoke `bar` and invoke `baz`. Everything is verified at compile time.\n\n  * If `bar` does not provide \"ensures\" contract that covers `baz`'s safety requirement:\n\nThen it's library A's author's responsibility to check it at runtime (which can make verification engine verify the safety requirement of `baz`).\n\n\n\n\ndlight:\n\n> `bar` should depend on a very specific version of `foo`, like `=1.2.3`.\n\nIf things work as I proposed above, then it's needless to pin the version or vender it:\n\n  * If `foo`'s author write verification contract, then if upgrading breaks, it is `foo`'s author's responsibility\n  * If `foo`'s author does not write verification contract, then `bar` should check it at runtime. Then upgrading will never be a problem.\n\n",
  "title": "Language vision regarding safety guarantees"
}