The Hyper-Card
If you are interested in learning how to program in the ACL2 subset of
Common Lisp, you might want to look at the following.
Maintenance of ACL2
It has been brought to our attention that the demise of Computational Logic,
Inc., has caused some potential users to shy away from ACL2 because of the
fear that it would not be maintained. Don't worry about that. The
``Boyer-Moore'' theorem prover has been maintained by its two authors (with
the help of a dedicated user community) for a quarter of a century without
any formal organization behind it. Indeed, that personal stake in the
``product'' is part of the reason Nqthm is rugged and reliable. Matt
Kaufmann and I have brought the same dedication and commitment to ACL2 (which
celebrates its 9th birthday on August 14, 1998.) We have been lucky to have
inherited many Nqthm users with their high expectations of reliability. We
see no reason why ACL2 will not continue to be maintained. There are many
reasons not to choose ACL2 as your theorem prover -- its relatively weak
logic, its style of user interaction, its syntax, etc., -- but its continued
maintenance is not among them.