Can you give an example of the kind of data-dependent behaviour you have in mind? We haven't implemented unions yet, but I see no reason why the approach we des

Can you give an example of the kind of data-dependent behaviour you have in mind? We haven't implemented unions yet, but I see no reason why the approach we describe in the article cannot propagate the tagging info in such a struct. As we explain in the article, Xr0's focus on formalising interfaces allows the verification of each function to be carried out independently. Thus we do reference counting only within individual functions. I'm not sure I fully understand the CPython example. What I can say is that the annotations allow us to capture the semantics such as whether a function destroys a value, stores its value in a global or returned value, or has no net effect on the state of its caller.