The magic wand P −∗ Q holds of resources that, joined with any disjoint resources where P holds, give resources where Q holds. It is a structure with a hole that P fills: a function's precondition is a wand to its weakest precondition, and a structure that lends out a part owns part ∗ part −∗ whole.

• Iris's triplesHoare triple IrisA Hoare triple {P} c {Q} says that if P holds when c starts and c finishes, Q holds when it does. Hoare logic gives one rule per construct: assignment substitutes into the postcondition, sequencing chains triples, a loop needs an invariant each iteration keeps. It is partial correctness: a run that never finishes satisfies every triple. and the continuation style of its specifications are wands: lst p xs -∗ cont -∗ WP … in the spike's sum_spec.

• Hello's quotearg returns a buffer that stays valid only until the next call with its slot; its specification lends it out, stringret ∗ stringret −∗ slots, which a first-order logic would have to encode. Campaign 4's libc contracts frame by hand instead: local_effect says a call changes only what its writable roots reach.

See How Iris works, Separation logic.