-In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable whose value is a pointer (i.e., an allocation-offset pair).
-Multiplying that integer by 2 leads to an error, because it is entirely unclear what it means to multiply such a pair by 2.
+In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
+However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
+
+This is the most lazy thing to do, and we do it because it is not clear what else to do -- in our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.
+Every allocation is just identified by an (unobservable) ID.
+We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
+The point it to discuss the *need* for such a model.
+If you are interested, I suggest you read [this paper](http://www.cis.upenn.edu/%7Estevez/papers/KHM+15.pdf) that explores the above idea of adding a base address.
+
+Long story short, pointer-integer casts are messy and hard to define formally when also considering optimizations like we discussed above.
+There is a conflict between the high-level view that is required to enable optimizations, and the low-level view that is required to explain casting a pointer to an integer and back.
+We mostly just ignore the problem in miri and opportunistically do as much as we can, given the simple model we are working with.