A 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.

• Iris writes a triple ⦃P⦄ e ⦃RET v; Q⦄ and defines it from the weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it., as □∀Φ, P −∗ ▷Q −∗ Φv −∗ WPe {Φ}: for any continuation Φ, owning P and the promise that Q gives Φ, e is safe and ends in Φ.

• Hoare logic breaks on pointers, because an assignment through one pointer may change what another names; separation logicseparation logic IrisSeparation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions. is the fix.

• nanofil's single-program proofs before the logic are Floyd's method: assertions at the points of a function, checked by never_panics_by_invariant (Cycle.v's cycle_never_panics).

See How Iris works, Hoare logic.