PIVOT, the program verification system written in BBN-Lisp by L. Peter Deutsch and described in his PhD thesis, “An interactive program verifier” is a recent addition to the Software Preservation Group web site.
Deutsch is a computer scientist who made important contributions to interactive implementations of Lisp and Smalltalk. While he was in high school, he implemented the first interactive Lisp interpreter, running on a DEC PDP-1 computer. While still in high school, he worked with Calvin Mooers on the design of TRAC, and implemented the language on a PDP-1 at BBN. Then Deutsch enrolled at the University of California at Berkeley, where he soon joined Project Genie, one of the earliest timesharing systems. Meanwhile, at BBN, Deutsch’s original PDP-1 Lisp became the “conceptual predecessor” of BBN-Lisp, running first on the PDP-1, then the SDS-940 (running the Project Genie timesharing system), and finally the PDP-10 running BBN’s own TENEX. After several of the BBN-Lisp creators, including Deutsch, moved to Xerox PARC, BBN-Lisp became INTERLISP. By this time, Deutsch had received his bachelor’s degree at Berkeley, and with other Project Genie alumni had co-founded Berkeley Computer Corporation, which built a large timeshared computer (the BCC-500) but then went bankrupt. While working at PARC, Deutsch also attended graduate school at Berkeley, carrying out the research on program verification that produced the PIVOT system.
Deutsch was kind enough to donate his only source listing of PIVOT to the Computer History Museum (Lot number X7485.2015), and to allow scans of the listing and his thesis to be posted on the SPG web site.