Prophecy Made Simple
Leslie Lamport, Stephan Merz · ACM Transactions on Programming Languages and Systems · 2022
Prophecy variables were introduced in the article “The Existence of Refinement Mappings” by Abadi and Lamport. They were difficult to use in practice. We describe a new kind of prophecy variable that we find much easier to use. We also reformulate ideas from that article in a more mathematical way.