Prove adequacy of observational view shifts
Prove an adequacy theorem that uses an observational view shift to establish that all the physical states during the execution of a program satisfy some property.
@swasey If you still want to do this, assign this issue to yourself, please.
One thing I have been wondering is whether this result should/could somehow be generalized to the case where some code has to run before the invariant we talk about is actually established. I think I have some idea(s) here, that should be fleshed out on a whiteboard.