hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Wh

hence if you are trying to prove anything about code in, say, C, you need to augment the code with explicit state and remove all non-local effects. (See: the Why language, which attempts to bridge this gap.) Actually, you just need to augment your model with notions of state, which is standard in operational semantics. It can just be harder to prove things in a complex model, so theorists prefer simplification when possible.