The latest update contains the first proof of Axiom's Common Lisp code using ACL2. ACL2 is a common lisp that has proof technology and since Axiom is all common lisp (no boot code), this is a good basis for proofs.
This update proves that the predicate isWrapped takes anything as an argument and returns either t or nil. One caveat is that ACL2 does not handle floating point so (floatp x) is omitted but this is fine for now. The signature line is isWrapped: t -> (or t nil) The plan of attack is to prove functions which use only common lisp primitives in their implementation first and then work upward through functions that use only the proven set. The base level functions are already marked in the interpreter. In the longer term ACL2 will be integrated into the build process so each release has an ever-growing proven subset. This is the first step in a very large task. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
