I'm not sure we're connecting. My point is that all of this low-level modeling of memory and pointers doesn't seem like it should be necessary in order to describe value semantics, and seems like it will result in a much more complicated model than necessary. Presumably you can describe a purely-functional system without introducing memory; that's just math. Then you can model mutation as the rebinding of variables to new immutable values, right?
I do think it's important to eventually be able to describe how types with value semantics can be built out of traditionally-unsafe parts like pointers and memory, but that doesn't seem necessary for the purposes of laying a foundation for value semantics. This post outlines my general thinking and might be helpful in setting the scene a bit.
Is what I'm saying here making any sense at all? It wouldn't be the first time I was completely misguided 