Posted on June 14, 2023 I’ve ported Swierstra’s 2009 proof pearl on the construction of the Hoare monad to SSReflect: see gist.