Two Kinds of Invariants: Safety and Validity

@RalfJung

I am glad to see that some of my previous ideas in comments on @nikomatsakis 's last blog post was presented in this blog. Specifically, the difference between ! and &!. I highlight the following:

while &! does not have a safe inhabitant, it is possible to have data that is valid for &! . After all, it does not have to point to a valid ! (which would be impossible).

For the same logic,

so validity for (T, U) requires that the first field is valid at T , and the second field is valid at U .

means (u32,!) is like !, it can never be valid.

Now the problem becomes: should we allow partial initialization on an invalid place?

I guess this also implies that partial initialization on invalid place should never be allowed, even in unsafe code.