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

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

A. Grant asks

"Why don't you like assertions enabling optimisation where
the compiler can prove the correctness of the assertion, i.e.
optimise it away?  Then all you are doing is giving a hint to
the compiler about an optimisation strategy, without altering
the meaning of the program at all."

There is nothing wrong with such assertions (they are typically called
pragmas in Ada for example), but they are TOTALLY different from the
kind of assertions that people want for debugging code.

Both uses are perfectly valid, but quite incompatible semantically, and
part of the trouble in designing facilities in languages for assertions
is that these two uses get badly entangled, both at the informal
discussion level, and at the formal semantic description level.

Actually there are many shades here. FOr example, to some people, 
assertions are things the compiler can trust regardless of proof
(some of the pragmas in Ada are like this too). To others, they
require proof as yu suggest and are merely hints to enable
otherwise allowed transformtaions of the code, to others they
are debuging statements to be executed at run time etc. etc.