The introduction of monads has two tremendous impacts on functional programming: 1) it provides a new way to structure functional programs; and 2) it enables efficient state manipulation by allowing in-place updates on the encapsulated state. In this talk, we are going to explore 2) by showing three correctness proofs in three different semantic models- the first one is based on a graph rewrite semantics which employs eager evaluation, the second one a natural semantics for lazy evaluation, and the third one a linear type system which has a hybrid evaluation strategy. How multiple named states can be handled in a monad will also be covered in this talk.