A predicate transformer semantics for effects (functional pearl)

摘要

Proving properties of imperative programs with side effects is quite arduous. Purely functional code, on the other hand, has a relatively pleasant equational theory that enables reasonable proofs. Is it possible to use modern machinery to make proofs about effectful programs easier? The work here illustrates such a path forward. As befits the pearl style, it walks the reader slowly and steadily through the ideas, with plenty of illustrative examples along the way. Complex ideas-the "predicate transformer semantics for effects" of the title, as well as a similar semantics for specifications and a way to mix them-are made quite clear. For the expert, various concepts from category theory that underlie the semantics are sprinkled throughout.