{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiafynficq3pm4qmdvh4biohjl5s2hwc5mbjed7dwsdgljo2kcvira",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mpjdgr3uglp2"
  },
  "path": "/t/language-vision-regarding-safety-guarantees/24418#post_15",
  "publishedAt": "2026-06-30T13:57:46.000Z",
  "site": "https://internals.rust-lang.org",
  "textContent": "tczajka:\n\n> So the difference is in whether you're careful enough in making sure the sorting algorithm is implemented correctly with no bugs?\n\nWhat's the difference between calling a safe function versus and unsafe function? Do you call the safe function if you're not careful enough to satisfy its requirements?\n\nHere's a thought experiment. You have a crate providing `fn sort(...)` and `unsafe fn sort_unchecked(...)` where the safety requirements are the logic requirements and which simply forwards to the safe function in the initial version, providing maximum flexibility:\n\n  * The author can use the safety requirements of the unsafe function to improve performance in the future in a compatible way.\n  * Users can choose to call a safe or performant version depending on whether they are careful enough.\n\n\n\nFor safety guarantees it's the same idea but where it's the author deciding whether they are careful instead of the client.\n\nToday, people usually consider that they should call the safe `sort` to avoid discharging requirements, because it's frowned upon to have to be careful avoiding bugs. But at the same time, they should be careful avoiding bugs when they provide guarantees, because anyone can use them to write unsafe code. This asymmetry doesn't make a lot of sense in my opinion. Users should be able to choose when and how much they want to be careful avoiding bugs, with the default of being fine writing bugs (i.e. safe by default).\n\nEvian-Zhang:\n\n> If an unsafe operation requires post-condition of an upstream crate:\n>\n>   * If the **safety** \"ensures\" contract from upstream crate covers such requirement, you don't need to do anything.\n>   * If not (either no safety contract or not cover), you must check it at runtime.\n>\n\n\nAgain, this looks good to me. But I'm still confused by:\n\nEvian-Zhang:\n\n> I do think there is few necessity of logic contract\n\nEvian-Zhang:\n\n> **try** to make logic correct with type system\n\nI agree. And the \"try\" is important. It's not enough. You can't encode your logic contract in the type system. So you can't make your logic contract a safety contract (since the type system is about safety, not logic).\n\nEvian-Zhang:\n\n> Secondly, even if we have logic contract, we can''t guarantee that a verified program is logically correct, but only guarantee that it works as we expected within modelled logic contract.\n\nWhat do you mean \"we can't guarantee that a verified program is logically correct\"? You can very well verify a program (and even crate) to be correct for logic. You'll need more than the type system, but you can.\n\nI'm also not sure what you mean by \"it works as we expected within modelled logic contract\". Do you mean we can only do dynamic analysis and not static analysis? This is not true. There are sound static analyzers for parts of Rust already (like VeriFast), and there's no theoretical reasons there can't be once Rust is fully specified.",
  "title": "Language vision regarding safety guarantees"
}