No subject

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.

* * *