Comment by tgv
5 days ago
As I see it: tracking (de)allocation in a very simple, understandable way. Unfortunately, that seems to be all it does. It's a start, certainly if you don't want to/cannot use a more complete system, since they can be quite complex. I'm not following this space professionally, only out of interest a bit, but do you know of a system that is so simple?
Xr0 isn't any simpler than for example Frama-C. In fact one of the simplest (but still useful) systems for statically tracking ownership is Rusts borrow checker, which the authors of Xr0 say is _too_ simple.