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

[ag129@ucs.cam.ac.uk (A. Grant)]

In article <qqn31rr53g.fsf@tartarus.ucsd.edu> djohnson@tartarus.ucsd.edu (Darin Johnson) writes:
>How about "Assert"!!!  That's exactly what this means in English,
>despite the fact that Ada changed its meaning.  "Assert" and
>"assertion" in English in no way mean "check that this is true".

If someone says something is true, don't you check it?  

There are all sorts of implicit assertions made by programmers
which the compiler doesn't have to believe.

  F(A,B(5),C/D)

implicitly asserts that F takes three parameters, that 5 is not out
of bounds for B, and that D is non-zero.  It is necessary for 
correct execution of the program (assuming we aren't relying on
trapping exceptions for the moment) that these be correct, so if
they can't be checked statically they should be checked dynamically.

Explicit assertions are just a way of doing the same for more
complicated algorithms where the compiler is unable to determine
for itself that some condition must be met for an algorithm to 
function correctly, or is unable to propagate implicit assertions 
backwards far enough to make the test as efficient as it could be.

The only situation where an assertion test is unnecessary is when
an assertion is guaranteed to be true by a proof that is too complex
for the program.  For example

  FUNCTION EXP(X)
  ... some polynomial ...
  EXP = ...
  RETURN

where you may want to assert in the published interface to EXP that
its result is positive.  I would suggest that any language environment
which supports this kind of unproved assertion must have linguistic
support (i.e. not just a comment) for reference to an external proof, 
e.g. a full record of the developer who made the assertion and any 
references they supply.

Again this is just like real life - if you can't see the truth of
someone's assertion, you have to see their evidence, and if you don't
understand it, but it is from a reputable source, you remember what 
it is in case you act on the assertion and get challenged.  Or you
at least get enough paperwork so that if the assertion turns out to
be wrong and your rocket explodes, they get sued, not you.