Axiom now has the necessary machinery to process proofs at build time (ACL2 for Lisp, COQ for Spad). While pondering the subject I ended up reading "The Semantics of Destructive Lisp"[0]. There is an interesting quote from Scherlis and Scott[1] which leads me to think there is a crossover from Collin's work on Cylindrical Algebraic Decomposition.[2]
The first thought involves the difference between a verification proof and a derivation proof. Verification involves proving an algorithm that already exists. Derivation involves transformations from an initial set to a final result. Both proofs work but [2] says "The traditional correctness proof -- that a program is consistent with its specifications -- does not constitute a derivation of the program. Conventional proofs, as currently presented in the literature, do little to justify the structure of the program being proved, and they do even less to aid in the development of new programs that may be similar to the program that was proved. That is, they neither explicate existing programs nor aid in their modification and adaptation. We intend that program derivations serve as conceptual or idealized histories of the development of programs. That is, a program derivation can be considered an idealized record of the sequence of design decisions that led to a particular realization of a specification. Stripped down to essentials, our claim is that the programs of the future will in fact be descriptions of program derivations. Documentation methods based on stepwise-refinement methodologies are already strong evidence that there is movement toward this approach. These documentation methods also provide support for the hypothesis that program derivations offer a more intuitive and revealing way to explain programs than do conventional proofs of correctness. The proofs may succeed in convincing the reader of the correctness of the algorithm without giving him any hint of why the algorithm works or how it came about. On the other hand, a derivation may be thought of as an especially well-structured constructive proof of correctness of the algorithm, taking the reader step by step from an inital abstract algorithm he accepts as meeting the specifications of the problem to a highly connected and efficient implementation of it." For mathematical algorithms, Mason [0] points out that it is possible to mechanically specialize an algorithm for a given case, often with an order of magnitude of efficiency. This is very appealing, especially in numeric domains where it can be proven that things cannot overflow. Collins works in semialgebraic sets, basically polynomials with a few comparison limits and parameters. CAD could be "bent" to use it as a compile step so that a CAD result would generate a program. Not only would this give a complete specification, it would provide a solid theoretical basis for the code. Can this be extended to derive other algorithms? Matrices can be viewed as polynomials. Can numeric algorithms be derived from the specification (e.g. LAPACK programs) that guarantee behavior? Much more reading to do... Tim [0] Mason, Ian A. "The Semantics of Destructive Lisp" CSLI Lecture Notes Number 5, ISBN 0-937073-06-7 (1986) [1] Scherlis, W. L. and Scott, D. S. "First Steps Towards Inferential Programming" in R. E. A. Mason (Ed.) Information Processing 83 New York, North Holland [2] Collins, George E. "Quantifier elimination for the elementary theory of real closed fields" Lecture Notes in Computer Science 33:134-183 (1975)
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
