  To demonstrate derivation of monadic programs, we present a specification of
sorting using the non-determinism monad, and derive pure quicksort on lists and
state-monadic quicksort on arrays. In the derivation one may switch between
point-free and pointwise styles, and deploy techniques familiar to functional
programmers such as pattern matching and induction on structures or on sizes.
Derivation of stateful programs resembles reasoning backwards from the
postcondition.
