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"