Hoare axioms have survived many challenges in the three decades since they were first published. This paper tackles another challenge: garbage collection. Collecting garbage invalidates some Hoare triples that involve the existence of objects.

To propose new semantics for existential quantifiers is the authors’ solution. One model is easy to understand; it depends on a correct and automatic garbage collector. An object is treated as existing if a possible heap (before garbage collection) could have contained it. The second is harder to understand. This one handles a heap with dangling pointers.

The paper will interest people who are studying program proving. Sections 1 through 7 could be read by a computer science graduate student who has studied formal methods and programming language semantics. Sections 8, 9, and 10 are increasingly more challenging; they demand familiarity with congruencies and knowledge of Kripke’s contributions to intuitionist logic. As the summary in section 11 states: “The...semantics will be unfamiliar to the...average program prover.” I suspect the average program prover prefers languages with safe garbage collection.

I like the way the authors share their enthusiasm for their subject. I’d like to see more on the connections between the logics of programs and topologies mentioned in section 10.