This can be done by taking Advantage of LISP's Theoretical Foundation.
As soon as pure LISP took its present form, it became apparent that properties of LISP functions should be provable by algebraic manipulation together with an appropriate form of mathematical induction. This gave rise to the goal of creating a mathematical theory of computation that would lead to computer checked proofs [McC62] that programs meet their specifications. Because LISP functions are functions, standard logical techniques weren't immediately applicable, although recursion induction [McC63] quickly became available as an informal method. The methods of [Kle52] might have been adopted to proving properties of programs had anyone who understood them well been properly motivated and understood the connections.
The first adequate formal method was based on Cartwright's thesis [Car77], which permits a LISP function definition such as
to be replaced by a first order sentence
without first having to prove that the program terminates for any lists u and v. The proof of termination has exactly the same form as any other inductive proof. See also [CM79].
The Elephant formalism (McCarthy 1981 forthcoming)
supplies a second method appropriate for
sequential LISP programs. Boyer and Moore [BM79] provide
proof finding as well as proof checking in a different formalism that
requires a proof that a function is total as part of the process of
accepting its definition.
I should say that I don't regard the LCF methods as adequate, because the ``logic of computable functions'' is too weak to fully specify programs.
These methods (used informally) have been succesfully taught as part
of the LISP course at Stanford and will be described in the textbook
(McCarthy and Talcott 1980). It is also quite
feasible to check the proofs by machine using Richard Weyhrauch's FOL
interactive proof-checker for first order logic, but practical use
requires a LISP system that integrates the proof checker with the
interpreter and compiler.
The ultimate goal of computer proof-checking is a system that will be used by people without mathematical inclination simply because it leads more quickly to programs without bugs. This requires further advances that will make possible shorter proofs and also progress in writing the specifications of programs.
Probably some parts of the specifications such as that the program terminates are almost syntactic in their checkability. However, the specifications of programs used in AI work require new ideas even to formulate. I think that recent work in non-monotonic reasoning will be relevant here, because the fact that an AI program works requires jumping to conclusions about the world in which it operates.
While pure LISP and the simple form of the ``program feature'' are readily formalized, many of the fancier features of the operational LISP systems such as Interlisp, Maclisp and Lisp Machine LISP [WM78] are harder to formalize. Some of them like FEXPRs require more mathematical research, but others seem to me to be kludges and should be made more mathematically neat both so that properties of programs that use them can be readily proved and also to reduce ordinary bugs.
The following features of present LISP systems and proposed extensions require new methods for correctness proofs: