From: Kaz Kylheku
Subject: Re: references/addrresses in imperative languages
Date: 
Message-ID: <1119323889.569038.39570@g44g2000cwa.googlegroups.com>
Lawrence D’Oliveiro wrote:
> In article <·······················@g49g2000cwa.googlegroups.com>,
>  "Xah Lee" <···@xahlee.org> wrote:
>
> >A[n] easy way to see this, is to ask yourself: how come in mathematics
> >there's no such thing as "addresses/pointers/references".
>
> Yes there are such things in mathematics, though not necessarily under
> that name.
>
> For instance, in graph theory, edges can be considered as "pointers".
> After all, make a change to a node, and that change is visible via all
> edges pointing to that node.

Oh yeah, by the way, note how such destructive changes to a variable
become whole-environment derivations in the discipline of proving the
correctness of imperative programs.

E.g. say you have this assignment:

   x <- x + 1

and you want to deduce what preconditions must exist in order for the
desired outcome   x = 42   to be true after the execution of the
statement. What do you do? You pretend that the program is not
modifying a variable in place, but rather manufacturing a new
environment out of an old one. In the new environment, the variable X
has a value that is one greater than the corresponding variable in the
old environment. To distinguish the two variables, you call the one in
the old environment X' .

You can then transform the assignment by substituting X' for X in the
right hand side and it becomes

  x <= x' + 1

and from that, the precondition  x' = 41  is readily deduced from the
x = 42  postcondition.

Just to be able to sanely reason about the imperative program and its
destructive variable assignment, you had to nicely separate past and
future, rename the variables, and banish the in-place modification from
the model.