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.

The ideas are made clear by explicitly showing Agda code (a dependently typed programming language in the Haskell family), along with explanations of each new idea. Full code can also be found online.

As system programming languages (such as Rust) give us more features for ensuring safety, we also need to keep looking ahead to the next level of features. Anyone who wants a clear preview of the bright future such investigations have should read this paper.