We were giving imperative programs formal semantics well before we started using monads. See Pneulli's "The Temporal Logic of Programs" (http://dimap.ufrn.br/~r

We were giving imperative programs formal semantics well before we started using monads. See Pneulli's "The Temporal Logic of Programs" (http://dimap.ufrn.br/~richard/pubs/dim0436/papers/pnueli_temporal_1977.pdf http://dimap.ufrn.br/~richard/pubs/dim0436/papers/pnueli_tem...) and Hoare's "An Axiomatic Basis for Computer Programming" (http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/pdf/Hoare_hist.pdf http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/p...). Monads are just one of many ways of formalizing notions of state. All of them have their tradeoffs. For example, in temporal logic it's much more obvious that "state does not compose" due to the frame problem.