Good insights -- and check out Alex Warth's "Worlds" paper on the Viewpoints site -- this goes beyond what PIE could do with "possible worlds" reasoning and computing ...
This is a very interesting paper. Its invocation of state space over time as a model of program side effects reminds me of an idea I had a couple years ago: if you think of a program as an entity in state-space where one dimension is time, then "private" object members in OO-programming and immutable values in functional programming are actually manifestations of the same underlying concept. Both are ways to create fences in the state-space-time of a program. Private members create fences along a "space" axis and functional programming creates fences along the "time" axis.
And you get to use "relational" and "relativity" side by side in a discussion.
A lot of interesting things tend to happen when you introduce invariants, including "everything-is-a" invariants. Everything is a file, everything is an object, everything is a function, everything is a relation, etc.