On Tue, Jan 22, 2008 at 02:43:42PM -0800, Andrew Lentvorski wrote:
avoided. Unfortunately, side-effects are often a great convenience when computational efficiency is important, and ``functions'' with side-effects are present in LISP. However, the so-called pure LISP is free of side-effects, and (Cartwright 1976) and (Cartwright and McCarthy 1978) show how to represent pure LISP programs by sentences and schemata in first order logic and prove their properties. This is an additional vindication of the striving for mathematical neatness, because it is now easier to prove that pure LISP programs meet their specifications than it is for any other programming language in extensive use. (Fans of other programming languages are challenged to write a program to concatenate lists and prove that the operation is associative).
Ocaml has a correctness prover that can be done for problems like this. It's called Coq <http://coq.inria.fr/>. The programs in Coq are a very small subset of ocaml, which is pure, but it certainly wouldn't be too difficult to prove list concatenation. A realistic list concatenation would use side effects for performance, however. Dave -- [email protected] http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-lpsg
