tweaks

[web.git] / ralf / _posts / 2022-04-11-provenance-exposed.md

diff --git a/ralf/_posts/2022-04-11-provenance-exposed.md b/ralf/_posts/2022-04-11-provenance-exposed.md
index b37344cc8a3715577b34dedb9a2cee828b9444aa..24b340236a37cf1e29d0c1e3d8dfc92075fbb6e2 100644 (file)
--- a/ralf/_posts/2022-04-11-provenance-exposed.md
+++ b/ralf/_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.