Please accept my reasons for asking the question, even if you disagree. I do not want this to evolve into a discussion about programming language design issues. Despite some familiarity with monads and the Haskell language, I am still of the opinion that alternatives should be explored.

The reference to Dijkstra's transformation rules indicates what I want to do. More explicitly I want to transform expressions in general, not just predicates. Also it 'hides states under the carpet' as I want. My interest is in programming language semantics and design. Model-based semantics strives to explain states, transformation-based strives to eliminate states. The latter potentially allows programs (including imperatives ones) to be transformed to pure mathematics.