[Haskell-cafe] Proving stuff about IORefs

[Derek Elkins]

On Sat, Oct 16, 2010 at 9:21 PM, Ben Franksen <ben.franksen at online.de> wrote:
> I have a formal proof where I am stuck at a certain point.
>
> Suppose we have a function
>
>  f :: IORef a -> IO b
>
> I want to prove that
>
>  f r == do
>    s1 <- readIORef r
>    r' <- newIORef s1
>    x <- f r'
>    s3 <- readIORef r'
>    writeIORef r s3
>    return x
>
> What happens here is that the temporary IORef r' takes the place of the
> argument r, and after we apply f to it we take its content and store it in
> the original r. This should be the same as using r as argument to f in the
> first place.
>
> How can I prove this formally?

You haven't provided us with any information about the formal model
you are using and your question is somewhat ambiguously phrased, hence
Thomas' response where, I'm pretty sure, he misunderstood what you
were asking.

At any rate, if you intend to prove this for any arbitrary f, I can't
tell you how to prove it formally because it's not true.

Regardless, this email has far too little information for anyone to
provide you an answer.