🚀 go-pugleaf

In article <31736@cornell.UUCP> bard@cs.cornell.edu (Bard Bloom) writes:
>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.
>
>Yes, yes, yes, we all know that, but what is the *proof* that there is no
>possible rewrite?  ... [discussion of operational and/or denotational
>semantics.] 

Golly, back when I was taking math courses rather than computer wonk stuff,
all of our proofs were informal.  The idea that long mechanical proofs are
even legitimate math has only recently come to be accepted in mathematical
circles and is still controversial.  (Is there any more reason to believe
that a 10,000 line mechanical proof is bug-free than that a 10,000 line
program is?)

In the case of the Algol 60 swap question, people long ago agreed that there
was no way to write a reliable swap, since the two arguments can affect each
other in arbitrary ways, the simplest example being swap(i, a[i]).  I
suspect you could show it's reducible to the halting problem.

By the way, A J Perlis once told me that when they defined call by name,
they thought that they were coming up with a more elegant refinement of call
by reference that avoided the need to define the semantics in terms of the
underlying implementation.  It wasn't until Jensen's device came along a
year or so later that they realized what a can of worms they'd opened.
-- 
John R. Levine, Segue Software, POB 349, Cambridge MA 02238, +1 617 492 3869
{ima|lotus}!esegue!johnl, johnl@ima.isc.com, Levine@YALE.something
Massachusetts has 64 licensed drivers who are over 100 years old.  -The Globe