Doesn't it blow your mind that you can represent imperative computations using a purely functional language? (like Haskell do-blocks, or lambda calculus itself).

The beauty of a declarative notation is not that you get to ditch representation of state, is that you can represent such state in a much more compact and tractable way than what is required by theoretical representations of imperative machines. Trying to do mathematical reasoning with Hoare logic is a pain in the ass.