Observational purity

[Don]

On 31.08.2011 09:35, bearophile wrote:
> Don:
>
>> If caching is the _only_ case which is required,
>
> They have developed this observational purity plus a way to enforce it, to allow static analyzability of contracts (so they are allowed to call only observationally pure methods), while keeping them flexible enough.

That's not the impression I got, though I didn't read it very carefully.
It seemed to me that what they have, is a runtime check (an assert that 
compares a read from a static variable, with a pure function; if they're 
the same, then the static variable isn't providing any extra state). The 
static analysis is used to ensure that the runtime check is always present.

They focused on the example of caching, but I found that a bit 
misleading, since you can easily get some kind of "real" purity in that 
case (there is no observable state AND there are no observable 
side-effects).
But this is not true of other forms of observational purity. I do not 
see how allowing a call to an impure function from inside a pure one, 
could ever be anything other than a convention. So I don't see how the 
logfile example could possibly be statically checked.