🚀 go-pugleaf

In article <1989Sep3.163014.4697@esegue.segue.boston.ma.us> johnl@esegue.UUCP (John R. Levine) writes:
>
>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.

I'd be quite happy with a proof in the usual mathematical style.  All the
proofs quoted so far are more along the lines of the old `proofs' of Euclid's
Fifth, the ones which eventually concluded "...which is repugnant to the
nature of the straight line."  Yes, there's something there, but it's not
right yet.

>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.

As usual, this is a persuasive informal argument, but it's not clear how to
formalize it in any nice way.  This "people long ago agreed" doesn't seem
quite up to the usual mathematical standards of proof. 

BTW, I'd be surprised if it were reducible to the halting problem (depending
on what "it" you're talking about) -- just a guess, but I have spent most of
my professional life (1) showing that things weren't definable in particular
classes of programming languages, and (2) reducing things to the halting
problem, especially to do (1).

>John R. Levine, Segue Software, POB 349, Cambridge MA 02238, +1 617 492 3869

Bard Bloom, Cornell University.