Lawrence D’Oliveiro wrote:

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.

Variables don't change in mathematics, at least the run-of-the-mill
everyday mathematics. :)

All these substitutions ``work'' in a way that is analogous to
functional programming. For example, substituting a variable into a
formula generates a new formula with occurences of that variable
replaced by the given value. You haven't destroyed the old formula.

Actually no. The process specifically avoids the pointer problem by
using an arithmetic coding for the formula, the Goedel numbering. The
formula talks about an encoded version of itself. That's how the
self-reference is smuggled in, via the Goedel numbering.

The final result just /is/ self-referential. It's not constructed bit
by bit like a data structure inside a digital computer that starts out
being non-self-referential and is then backpatched to point to itself.

A mathematical derivation may give you the idea that something is
changing in place, because you always hold the most recent version of
the formula at the forefront of your mind, and can visualize the whole
process as a kind of in-place animation in your head. But really, at
each step you are making something completely new which stands on its
own.

Is that so? That implies that there is some table where you can
associate names (or whatever type of locators: call them pointers,
whatever) with arbitrary values. But in fact that's not the case.

Nope. Goedel didn't add anything, he just revealed what was already
there: that you can have statements of number theory, well-formed
formulas constructed out of existing operators without any backpointer
tricks, which have true interpretations, but are not theorems.

Everything in a Goedel's string can be recursively expanded to yield an
ordinary formula! There is no infinite regress, no unchased embedded
pointer-like things left behind.

Self-reference is achieved using two tricks: Goedel numbering, and
indirect reference. Godel numbering allows a formula to talk about
formulas, by way of embedding their Godel numbers, and translating
formula-manipulations into arithmetic manipulations (of interest are
finite ones that will nicely unfold into finite formulas). In essence
that which used to be ``code'' can be now treated as ``data''', and
operations on code (logical derivations) become arithmetic operations
on data.

Indirect reference is needed because a formula G's Goedel number cannot
be inserted into itself directly. If you start with a formula G which
has some free variable V, and then produce some new formula by
substituting G's Goedel number into it directly for occurences of V,
you no longer have G but that other formula.  You want whatever comes
out to be G, and so the input formula, the one with the free variable,
cannot be G, but perhaps a close relative which either talks about G,
or whose constituent formulas cleverly end up talking about G after the
substitution takes place.

Instead of a direct (Goedel number) reference, you can insert into a
formula some /procedure/ for making that formula's Goedel number out of
another formula's Goedel number and talk about it that way. As an
example, instead of saying ``here is a number'' by inserting its
literal digits, you can say ``the number that results by applying this
formula to this other number''. For instance, instead of writing the
number 4 we can write   successor(3). or   2 + 2.   We explicitly
mention some other number, and say how 4 is constructed out of it.

Douglas Hofstadter exposition of all this is very good. To allow the
formula G to mention its own Goedel number, Douglas Hofstadter uses
another formula which he calls U, the ``uncle''. The trick is that: the
procedure for making G's Goedel number out of U's number is the
arithmetic equivalent of the same procedure that's used to substitute
the Goedel number of U for the free variable in U itself. So as U (the
formula) is treated by substituting its own Godel number for its one
and only free variable, it produces G, and, at the same time, the
arithmetic version of that substitution, fully contained inside the U
formula itself, turns the now substituted copy of U into G also.  U
contains the fully expanded ``source code'' for the arithmetic version
of the free-variable substitution procedure, and it contains a free
variable representing the arithmetic version of the formula on which
that algorithm is to be done. As that free variable within U is
replaced by the Goedel number U, the overall formula becomes G, and the
embedded free-variable-replacement procedure is instantiated concretely
over U's Goedel number, so it becomes a constant, unparameterized
calculation that produces G's Goedel number.

Voila, G contains a procedure that computes the arithmetic object
(Goedel number) that represents G's ``source code'' (the symbolic
formula), out of the embedded number representing U's source code.
Using that giant formula, G can assert things about itself, like ``I am
not a theorem'' (i.e. ``there exists no integer representing the Goedel
numbers of a list of true statements that represent a derivation
deducing myself as the conclusion'').

There are no name references or pointers or anything. All the functions
are primitive recursive, and so can be expanded into finite-length
formulas which contain only numbers and operators and variables---dummy
ones that are bound to existential quantifiers, not to concrete values
some external name/value table.