[plt-scheme] to define, or to let

Matthias Felleisen wrote:
> My general position is that programming is equally about correct
> and incorrect programs. Scripting is fun. Writing programs in a
> dynamically typed language is fun. But as the programs "grow" up,
> they need more and more stability. That means, we must be able to
> equip the language with tools that help us discover errors and
> that help us describe our thoughts.

I agree.  "Help us discover errors and help us describe our thoughts" is
key.

> A language [family] as weakly specified as R5RS is not a
> good basis for this "growing up business."  It starts with
> the unspecified order of evaluation and continues with
> all the other places where R5RS is wishy-washy about errors.

I see a conflict here, between this formally-based perspective on order of
evaluation, and what is encountered in real systems.

 From the formal perspective, fixing the order of evaluation produces a
language that is simpler to analyze and prove properties about (or something
along those lines).

However, from the perspective of a real-world user of this language, a
working program may nevertheless contain inadvertent order dependencies -
dependencies which exist, and which are satisfied by the fixed order of
evaluation, but that the author of the program did not intend.

The formal perspective on this situation is that such dependencies are
perfectly valid, with respect to the language.  The notion of the intent of
the programmer, with respect to order of evaluation, does not exist in the
language, and as a result nothing can be said about it formally, at that
level.

(To connect to the run-away regimes and civil disobedience metaphor used
earlier, we're now talking about censorship of the most Orwellian kind -
changing the language to prevent expression of undesirable information.
However, we can't change the reality which the system has to deal with -
inadvertent order dependencies still exist, even if we're not allowed to
talk about them.)

The problem is that inadvertent order dependencies can and do lead to bugs
in the real world, even though the language "pretends" that such cases are
valid code.  A model theorist might say something along the lines that the
the domain of real systems is not a model for the language (hope I didn't
mangle that too badly).  Perhaps the claim should not be so broad, but
there's clearly something missing in the mapping here.

* * *

 From the real world perspective, if we're "growing up", do we want this sort
of incompleteness in our systems?  In truly mission-critical software (as
opposed to mere commercial systems in which the worst consequence of error
is some lost money), it would be disturbing to find that unintentional and
unnoticed dependencies were being addressed by automatically satisfying
them, even if we don't know where they are and haven't examined them.

I'd be concerned that these may cause latent errors to be uncovered by some
unexpected data inputs (think Ariane 5), or by a code change that should
have been innocuous, if not for an unnoticed dependency.  Rather than paper
over such potential errors and ignoring them, I would prefer to have a means
to stress-test code which claims to be free of order-dependencies.  To do
that, we need the means, in the language, for making the claim of
order-independence in the first place (a "declaration of independence", from
the Orwellian regime mentioned above).

It would seem strange that formal analysis is telling us that a language has
been made safer by fixed evaluation order, while real-world experience may
tell us otherwise - but this dichotomy is explained by the mismatch between
real systems, and the simplified language.

It's only by meta-sleight-of-hand that our focus has been redirected to a
narrower system.  We can't assume that safety within that system says
anything about the safety of real systems.

Of course, the basic issue is still the same - a subjective tradeoff between
pros and cons on either side.  I can see why semanticists would like the
simpler, more tractable system.  However, with the possible exception of
systems amenable to correctness proofs, it's not at all clear to me that
fixed evaluation order is on the side of real-world safety.

If there is under-specification present here, surely it is actually in the
language which disallows the specification of order independence, despite
such order independence being a manifest property of large parts of real
world systems?

> Is it possible to provide a complete specification of a language?
> I don't know. Languages are huge, complex artifacts. Take a look
> at the number system. Take a look at thread systems and similar
> things. I don't know whether we can do an adequate job. But that
> shouldn't prevent us from doing better than we have done in the
> past.  That's part of what PLT is about and I sure hope we can
> stay the course.

No argument there.

Anton