Re: next "big" language?? (disagree)

[dewar@cs.nyu.edu (Robert Dewar)]

Jon said

"I have to agree with Jon's point here.  I don't see any reason why the
definition of the language would have to prevent the compiler from
using the information for optimization.  If the customer didn't want
that to happen, the vendor could add a command-line option or pragma
to tell the compiler not to.  Don't Ada compilers already have
command-line options and/or pragmas to control how much optimization
takes place, anyway?"

This is really quite a tricky and subtle issue. If you do not see any
problem, then it is likely you don't see the issues fully yet. The basic
problem is that the notion of assertion can mean many things, and at the
level of discussing the precise semantics of assertions, there are
fundamental disagreements. There is certainly a school of thought that
is insistent that it is crucial that assertions NOT affect the semantics
or even the behavior of the program. 

You can declare this silly if you like, but it is more helpful if everyone
makes the effort to understand the issues.

In GNAT, 

   pragma Assert (X);

means EXACTLY

   if not X then
	raise Assert_Error;
   end if;

which is well defined, but not at all in the category of assertions that
the compiler can take advantage of, which can behave in a completely
differrent (and possibly suprising manner).

For instance, another view of assertions is exemplified by the following:

    pragma Assert (X /= 0);
    ...
    Q := 30 / X;

where the compiler "knows" that X is non-zero, and therefore skips the
test for X being zero in the division, and consequently generates some
junk value in Q. In this model, assertions do not correspond to any
executable code.

There is nothing wrong with either of these models of assertions (or with
any of several different models), but they are VERY different, and what we
found in practice is that people had very strong opinions that an assert
in the language should mean one or other of these, and that it was silly
to suggest any alternative meaning -- not exactly a recipe for agreement,
or for the devising of a language feature that would not cause a lot of
confusion.

I expect most Ada 95 compilers will copy the GNAT pragma Assert, but this
is of course only one possible interpretation of this notion (it happens
to be one whose semantics are very easy to describe, but it is not necessarily
what everyone wants!).