[Tarean]

Sometimes keeping a fixed shape for the variable context across the computation can make it easier to reason about invariants, though.

Like, if you have a constraint is_even(x) that's really easy to check in your head with some informal Floyd-Hoare logic.

And it scales to extracting code into helper functions and multiple variables. If you must track which set of variables form one context x1+y1, x2+y2, etc I find it much harder to check the invariants in my head.

These 'fixed state shape' situations are where I'd grab a state monad in Haskell and start thinking top-down in terms of actions+invariants.