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

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

In article <dewar.834584250@schonberg> dewar@cs.nyu.edu (Robert Dewar) writes:
>A. Grant said
>"The point of assertions is not to print messages for the
>programmer.  You can use them to allow the compiler to
>optimise safely..."

>It is certainly true that assertions can be used for compiler optimization,
>but that's not what people want.

What people want is for the compiler to do all the work, i.e. prove
that all array subscripts are valid, that all dereferenced pointers
are non-null, that all division denominators are non-zero etc.
I think realistically, compilers can be helped by assertions which 
indicate stages in the proof, to do optimisations which they wouldn't
otherwise be able to.  Especially inter-procedural or inter-module
optimisation where the assertion forms part of the interface.

>When we discussed putting pragma Assert into the language

Are you reading this in comp.lang.ada?  I didn't mean to refer to
any particular language.

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.