AllGoodAlg proof outline

• The proof is done by structural decomposition.
  • The basic operations preserve the invariant.
  • The combinators produce results that preserve the invariant if the parts preserve the invariant.
• The basic operations are reads and writes in the protected memory monad.
• The combinators used include monadic combinators like, >>=, liftM and return.
• The properties required of the combinators are essentially the free theorems for the respective types.
• No monad laws needed to be proved or referenced explicitly.