{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreige5cbzdkczbeq6gpdvt7oilmkmlaxepsj45njgapjopre63htwwi",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mn6fjqel5td2"
  },
  "path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=3#post_41",
  "publishedAt": "2026-05-31T18:26:45.000Z",
  "site": "https://internals.rust-lang.org",
  "textContent": "ais523:\n\n> Or in other words, I don't see the angelic choices as being made immediately. Rather, I think that sort of choice works like variables in Prolog:\n\nYou are describing something more akin to symbolic execution than angelic choice. Symbolic execution is indeed a way to approximate or even implement angelic choice. But having that in an actual program run (rather than in a program analyzer) requires explicitly adding symbolic state to the program state, which in turn affects everything else that reasons about the program state.\n\nFor ptr2int casts specifically, the PNVI-ae-udi model in C does pretty much that: the \"udi\" mechanism introduces a symbolic form of provenance that approximates the angelic semantics. Sadly it does not easily work with more complicated models such as Stacked/Tree Borrows, or even with `restrict` in C.",
  "title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}