From: Ralf Jung Date: Tue, 12 Apr 2022 12:38:10 +0000 (-0400) Subject: tweaks X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/2df7cf7d96f06427c1b4608dd754bd0023f1e1bc?ds=inline;hp=ff69fd7e17ea1b60014a7cb42fa8209ffb5276b1 tweaks --- diff --git a/personal/_posts/2022-04-11-provenance-exposed.md b/personal/_posts/2022-04-11-provenance-exposed.md index b37344c..24b3402 100644 --- a/personal/_posts/2022-04-11-provenance-exposed.md +++ b/personal/_posts/2022-04-11-provenance-exposed.md @@ -345,8 +345,8 @@ Here, too, my vision for Rust aligns very well with the direction C is taking. (The set of valid guesses in C is just a lot more restricted since they do not have `wrapping_offset`, and the model does not cover `restrict`. That means they can actually feasibly give an algorithm for how to do the guessing. They don't have to invoke scary terms like "angelic non-determinism", but the end result is the same -- and to me, the fact that it is equivalent to angelic non-determinism is what justifies this as a reasonable semantics. -Presenting this as a concrete algorithm to pick a suitable provenance is then just a stylistic choice. -Kudos go to Michael Sammler for opening my eyes to this interpretation of "user disambiguation".) +Presenting this as a concrete algorithm to pick a suitable provenance is then just a stylistic choice.) +Kudos go to Michael Sammler for opening my eyes to this interpretation of "user disambiguation", and arguing that angelic non-determinism might not be such a crazy idea after all. What is left is the question of how to handle pointer-integer transmutation, and this is where the roads are forking. PNVI-ae-udi explicitly says loading from a union field at integer type exposes the provenance of the pointer being loaded, if any.