Newsgroups: comp.lang.scheme
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!caen!news.cs.indiana.edu!hieb@heston.cs.indiana.edu
From: Robert Hieb <hieb@heston.cs.indiana.edu>
Subject: Re: Fixing the order of evaluation. Minimizing the unexpected.
Message-ID: <1991Apr10.173308.4035@news.cs.indiana.edu>
Organization: Computer Science, Indiana University
References: <KERS.91Apr9082505@cdollin.hpl.hp.com> <9104101634.AA24470@garlic.Stanford.EDU>
Date: Wed, 10 Apr 91 17:32:51 EST

mkatz@garlic.stanford.EDU (Morris Katz) writes:


>      ((lambda (a b) -X-)  -A-  -B-)   =   ((lambda (b a) -X-)  -B-  -A-).

>   [1] But, in an imperative language, it *already* isn't; never mind the
>   lambda's, the arguments have to be evaluated in *some* order, and different
>   orders may may a difference. So [1] is a lost cause.

>Not true!  If argument evaluation order is unspecified then only an incorrect
>program will file to meet property [1]

Not not true!  I find no such stipulation in R^3.99RS.  It simply says
that the order of evaluation of the operator and operand expressions of
a procedure call is unspecified.  So, for instance, assuming a
pseudo-random number generator,

        ((lambda (a b) (cons a b)) (random) (random))

may be perfectly "correct" without being equivalent to

        ((lambda (b a) (cons a b)) (random) (random))

Presumably one does not care exactly what one gets for "a" and "b."
Yet one might still wish to get the same thing when one runs the
program on different Scheme systems, or different versions of the same
Scheme system.

In the end, the strongest argument for complete language specification
is verification by testing, rather than verification by proof.  If one
is trying to prove a program is correct by more or less formal methods,
one can start by establishing that the program doesn't rely on
unspecified behavior.  Then one can proceed with a simpler proof that
doesn't take into account argument evaluation order, or other such
unpleasant realities.

However, such techniques are finally unsatisfactory, no matter how
formal.  There is no reason to assume that a proof will be simpler than
a program, after all.  One must prove the proof, prove that the program
is implemented as specified, etc.  And do so again each time the
program is modified.

There is no substitute for testing a program.

The confidence attained by testing is proportional to the completeness
of the language specification.  I guess no one will ever want to use
Scheme to control airplanes or power plants so we don't have to worry
about that...