In the Spring of 1996 Computational Logic received an extremely small contract from the Office of Naval Research, designed to support a high school student over the summer learning ACL2. CLI charged no overhead nor profit on this contract. Our supervisory time was donated.
This report is the student's summary of his experience. (A postscript version is also available.)
It is our belief that things were working quite well up until his final assignment, which was too large a leap for him to successfully make on his own.