Aliasing is very hard to reason about formally, because no matter what you do, you start running into the undecidability issue. Sure, but we're talking about alias *sets*, which is a different issue.