AllGoodAlg proof outline

• The previous slide showed that >>= and return preserve the MostlyStateIndependent property.
• The proof of AllGoodAlgs consists of analogous proofs that the other monadic operations used in the definition of doPacket also preserve the MostlyStateIndependent property.
• There are similar definitions for the protected memory monad.

What if?

• If the code was more polymorphic, would the free theorem for the type of doPacket be all we need?