I’m not quite sure what the point is here. I agree that well written imperative code can be easy to read, and that it’s often the natural style for many problems. I just think it’s always better to use that style in a system that makes the available context explicit and enforces a strict discipline via the type system (e.g. a State monad).

Regarding semantics my experience is that defining formal semantics for languages with unrestricted mutation (or even worse aliased pointers into mutable state) than one that avoids those features.