If you're hell bent on functional style, you can represent memory writes as ((Address, Value, X) -> X), where X is a compile-time-only linear type representing the current memory state, which can be manipulated like any other SSA variable. It makes some things more elegant, like two reads of the same address naturally being the same value (as long as it's reading from the same memory state). Doesn't help at all with aliasing analysis or write reordering though so I don't think any serious compilers do this.