[Haskell-cafe] Re: Proving stuff about IORefs

[Malcolm Wallace]

>>> 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.
>
> How do you know that? Can you give an example where it fails?

The problem with the code you originally posted was that it looked  
like this:

   f r = do r' <- something
            f r'
            something else -- this is dead code

That is, the computation is non-terminating, because f simply calls  
itself recursively, with no base case.

Regards,
     Malcolm