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

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

Dale said

"Obviously if there are two concepts, then we should have two names. For
example (in Ada) we could stick with

        pragma Assert(x);

for the traditional "please check this really is the case" assertion
and introduce

        pragma Fact(x);

(or some other name) for the "this really is true, trust me, and make
appropriate optimisations" type assertion. Can anyone think of a better
name (pragma Declare(x) is not available in Ada) than "Fact"?"

Sure this is one approach, but WG9 felt it was over-complex to introduce
multiple concepts here, especially when it is essentially impossible to
come up with non-confusing names (since assert is the obvious name for
all cases).

Note too that the pragma Assert in GNAT, which is equivalent to an if
statement with a raise, is still not what some people want, since of
course the optimizer can and does derive some information from the
presence of the Assert. What some people want is an Assert that is
guaranteed to be semantically non-intrusive -- a rather slippery
concept.

Anyway, in practice I think that the assert of GNAT is as far as it is
reasonable to go. At least the advantage of the GNAT definition is that
its semantics is trivially simple (since it is defined by the equivalent
if/raise sequence).

There just does not seem to be enough consensus to go further, unless you
really go to full annotation, in for example the SPARK style using the
Praxis tools. For this pragma Annotate, as recently recommended by the
HRG to WG9, and as currently implemented in GNAT, can be used.