@saikou@gts.chuuni.solutions All of this work is very closely connected to other work on typestate, which could loosely be defined as a flavor of flow-sensitive typing that is based around the idea of a protocol of valid states/transitions on a variable/object. Traditional typestate is very non-monotonic (since it wanted to enforce that resources are appropriately released), whereas initialization analysis in the context of Java is monotonic. However, in a systems language you might want to uninitialize a field that was previously initialized. I was trying to find a particular reference that isolates this point, but with typestate you don't need to expose information about the actual fields of your module's abstract types. Instead, you can expose the types along with an abstract (semi)lattice of potential states and annotations indicating how your public functions transition between states.