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_tem...) and Hoare's "An Axiomatic Basis for Computer Programming" (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.