The only limitation to the allocation patterns Xr0 imposes is that there can be no leaks. Everything else is possible.
Yes, Xr0 is young. It took Rust nine years to reach v1.0.0. Xr0 may need slightly over the nine months its had.
Yes, Xr0 is young. It took Rust nine years to reach v1.0.0. Xr0 may need slightly over the nine months its had.
I am curious to know how you would handle tagged unions, say, something like this:
struct object {
int type; /* OBJ_INT, OBJ_STR, etc. */
union {
int i;
char *s; /* heap allocated */
/* etc */
} val;
};
How would you model things like reference counting? In CPython, for example, one of the most pernicious programming problems is invalid reference counting because the C API functions are rather inconsistent in their handling of reference counts. One has to carefully peruse the documentation to understand if the function will steal a reference (from a parameter), borrow a reference (for the return value), or if it makes a new reference. Such setups are perfect candidates for annotation.
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.