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

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

In article <4plaa6$c7a@goanna.cs.rmit.EDU.AU> rav@goanna.cs.rmit.EDU.AU (++           robin) writes:
>        ag129@ucs.cam.ac.uk (A. Grant) writes:
>        >>   if mod(x, 2) ^= 0 then
>        >>        put ('The value of x is not odd.');

>        >The point of assertions is not to print messages for the 
>        >programmer.

>---If you don't tell the programmer that something is wrong,
>there's really little point in putting
>extraneous clutter in the program.

You really don't understand do you?  An assertion isn't meant to fail. 
If it ever does fail it should do more than print a message to the user 
(how is it meant to print a message to the _programmer_?) -- a full
traceback and dump would be more useful, followed by error recovery.
It should not continue with execution of the following code if that
is making assumptions based on the assertion being true.

>        > You can use them to allow the compiler to 
>        >optimise safely, provide a contractual interface between 
>        >modules, and for preconditions, postconditions, loop invariants
>        >etc. when proving the correctness of programs.
>        >E.g. the assertion that X is odd could form part of the 
>        >declared interface to a module whose implementation was hidden.  

>---That may be so, but if the program doesn't feed the
>fact that there is a violation, then there's no point in the
>program.

The idea is that assertions are a static property of the program,
like a more complex form of typing (see someone else's post above).
Ideally you should be able to go through your program and prove 
that all your assertions are satisfied without the need for any
runtime tests at all.  Then you can compile without assertions.
A clever compiler might be able to prove things too.

Surely the concept of formal proof of programs is familiar to
anyone at RMIT?  What exactly is your position there?