🚀 go-pugleaf

In article <8369@boring.cwi.nl> dik@cwi.nl (Dik T. Winter) writes:
> [vanilla swap procedure, and example using side effects and arrays]
>will not swap x[1] and y[1], but y[1] will be stored in x[2] and
>x[1] will be stored in y[2], and there is no possible rewrite of swap
>that corrects this.
>dik t. winter, cwi, amsterdam, nederland

Yes, yes, yes, we all know that, but what is the *proof* that there is no
possible rewrite?  The informal argument is pretty simple -- to write
swap(x,y), you need to reference each of x and y twice, and all kinds of
things can happen between the references, and we all know that as well.

I'm trying to track down the theorem and its proof.  Trying to formalize that
"you need to reference..." line is rather hard.  

The theorem I want says "There is no possible integer swap routine."  This
presumably requires quantifying over all possible code bodies, somehow. 
The only proof methods I can think of are:

  1) Grind through the operational semantics of Algol.  This sounds like a
     real demon.  I haven't a clue about what the right induction hypothesis
     might be.

  2) Conjure up an adequate denotational semantics for Algol in which there
     is no integer swap routine.  

Neither one of these sounds elementary.  When I've heard the fact stated, it
sounded as if it had an elementary proof and not just a plausibility
argument. 

-- Bard