Assertion languages, optimisation & proof

[David Glen JEFFERY]

Hi all,

The goals of introducing these assertion declarations seem to have become 
much broader. (FWIW, I think that this is definately a good thing. If we can
avoid having to add different syntaxes for a billion little things as they crop
up, then that's a great thing. I particularly like Peter Schachte's suggestion
for having named assertion patterns such as ``associative''). We have moved
from just wanting a way of asserting that a predicate is associative to
wanting an assertion language which describes (almost) arbitrary properties
of programs.

So... on to my point. Some of the potential uses for these assertions that
have cropped up in discussions are:
	- To allow the compiler to optimise certain programs where the
	  optimisation relies upon a particular property. (eg. accumulator
	  introduction, which relies on associativity)
	- for input and output assertions for predicates
	- for imposing invariants on types. (BTW, wouldn't it be cool to make
	  io__read fail if the term it read in didn't satisfy the invariants?)

Doing the first is conceptually simple: we are providing annotations which
give information about the program (which the compiler may or may not try to
prove), and the compiler is free to do whatever it will with them. There is no
visible change to the programmer apart from the fact that the compiled program
may now run faster.

My question concerns the last two (invariants on preds and types). If we
only use these kinds of assertions for optimisation (eg. optimising away
call to error/1), then there is no conceptual problem. However, if we are
going to use this "meta-language" of assertions for proving properties of a
program which potentially affect program correctness, we need to be more
careful since we are changing the definition of static program correctness.

For example, the fact that two lists are always the same length may make
a predicate which is semideterministic in the eyes of the compiler into
a determinstic one. When we start doing this kind of thing, we need to be
*very* careful in stating how clever the compiler is. We need to state exactly
what proof methods the compiler uses to prove which properties since
a programmer needs to be able to predict whether or not a program will
compile without actually running it through the compiler.

So finally... my point: Do we want to complicate the language definition and
consequently constrain any future Mercury implementations to have to do some
pretty tricky things, or should we only use assertions for non-user visible
optimisations?

(I don't mean to be negative about the idea... in fact I really hope we can
work out a simple, powerful system that we can include in the language. It 
would certainly be a bonus as far as program reliability goes.)


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.