Proofs and development

[Alan Grover]

In one of the chapters of the Clean book, some functions are transformed to
be more efficient. The author then shows by proof that the new functions
are equivalent to the old. The exercize is supposed to demonstrate that
performance is a concern after the algorithm is shown/known to be correct.

I heartily endorse this, but would like the language to help me out.
Similar to the book example, I would like to write my program/functions
worrying only about correctness. Then I could analyze the performance. I'd
then like to modify the source code adding the better algorithm, but I'd
like to keep the original algorithm as the documentation. The
language/system should then help me prove that the better version is
equivalent. I feel that this helps keep the source code understandable, and
connects it more directly with the requirements and specifications.

Here's the kind of thing I'd like in the source:

// This is the "direct" version of the function
// It should be as obvious and self explanatory as possible
// This one isn't actually compiled
Prototype
funGifnarb x y = blah blah blah
	where
		blah = blah
		blah = blah
		etc.

// This is the "improved" version.
// The Clean system will help me prove that this
// is equivalent to the above, and then this is
// compiled
funGifnarb x y = homina homnia phbbt
	where
		homina = goo goo goo
		phbbt = la la la

I think that in some cases, mechanical reasoning alone could prove the
equivalence (certain simple cases). I suspect that the programmer will have
to supply help in a lot of other cases. In addition, laws and lemmas will
have to be supplied to support the reasoning.

This all has relation to literate programming, does anyone else have
interest in that?

---
"Alan Grover, Technical Pb" awgrover@umich.edu
+1 (743) 647-5778
Project Leader
Health Media Research Lab, Cancer Center
5D04 North Ingalls Building, Mail Stop 0471
300 North Ingalls
Ann Arbor, MI 48109-0471