"Simon Marlow"
I should have said that if 'acts' blocks, then the transformation is invalid.
Well that is exactly what I was assuming when I said that the transformation is invalid. In the general case, for some arbitrary actions between the write and the read (excluding another write of course), there is no guarantee that the IORef remains unmodified. If you want to restrict the intermediate actions to be non-blocking, such that another thread cannot run, then that is an extra (and significant) proof obligation. And AFAICS your non-blocking argument only applies to co-operative scheduling. If pre-emption is permitted (e.g. interrupt-handling), then all bets are off, because an arbitrary thread could write to the IORef at any moment.
I don't think so. Malcolm asserted that the transformation was invalid in a multi-threaded implementation; I disagree - it's just as valid in a multi-threaded implementation as a single-threaded one.
I think what I said was correct in general. You need quite a lot of side-conditions to assert the opposite. Regards, Malcolm