{"id":810,"date":"2015-05-14T12:55:04","date_gmt":"2015-05-14T20:55:04","guid":{"rendered":"http:\/\/www.mcjones.org\/dustydecks\/?p=810"},"modified":"2018-06-10T16:24:40","modified_gmt":"2018-06-11T00:24:40","slug":"l-peter-deutschs-pivot-program-verification-system","status":"publish","type":"post","link":"https:\/\/mcjones.org\/dustydecks\/archives\/2015\/05\/14\/810\/","title":{"rendered":"L. Peter Deutsch&#8217;s PIVOT program verification system"},"content":{"rendered":"<p><a href=\"http:\/\/www.wheels.org\/spacewar\/stone\/rolling_stone.html\"><img decoding=\"async\" align=\"right\" src=\"http:\/\/www.wheels.org\/spacewar\/stone\/deutsch.jpg\" alt=\"L. Peter Deutsch in his office at Xerox PARC, around 1972.\" \/><\/a><a href=\"http:\/\/www.softwarepreservation.org\/projects\/verification\/pivot\/\">PIVOT<\/a>, the program verification system written in <a href =\"http:\/\/www.softwarepreservation.org\/projects\/LISP\/interlisp_family#BBN_LISP_\">BBN-Lisp<\/a> by <a href=\"http:\/\/c2.com\/cgi\/wiki?PeterDeutsch\">L. Peter Deutsch<\/a> and described in his PhD thesis, &#8220;<a href=\"http:\/\/www.softwarepreservation.org\/projects\/verification\/pivot\/Deutsch-An_Interactive_Theorem_Prover-1973.pdf\/view\">An interactive program verifier<\/a>&#8221; is a recent addition to the <a href=\"http:\/\/www.softwarepreservation.org\/projects\/\">Software Preservation Group<\/a> web site.<\/p>\n<p><a href=\"https:\/\/en.wikipedia.org\/wiki\/L_Peter_Deutsch\">Deutsch<\/a> 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 <a href=\"http:\/\/www.softwarepreservation.org\/projects\/LISP\/interlisp_family#Basic_PDP-1_LISP_\">interactive Lisp interpreter<\/a>, running on a DEC PDP-1 computer. While still in high school, he worked with <a href=\"http:\/\/conservancy.umn.edu\/handle\/11299\/107510\">Calvin Mooers<\/a> on the design of <a href=\"https:\/\/en.wikipedia.org\/wiki\/TRAC_(programming_language)\">TRAC<\/a>, and implemented the language on a PDP-1 at BBN. Then Deutsch enrolled at the University of California at Berkeley, where he soon joined <a href=\"https:\/\/en.wikipedia.org\/wiki\/Project_Genie\">Project Genie<\/a>, one of the earliest timesharing systems. Meanwhile, at BBN, Deutsch\u2019s original PDP-1 Lisp became the &#8220;conceptual predecessor&#8221; of <a href =\"http:\/\/www.softwarepreservation.org\/projects\/LISP\/interlisp_family#BBN_LISP_\">BBN-Lisp<\/a>, running first on the PDP-1, then the SDS-940 (running the Project Genie timesharing system), and finally the PDP-10 running BBN\u2019s own <a href=\"https:\/\/en.wikipedia.org\/wiki\/TOPS-20#TENEX\">TENEX<\/a>. After several of the BBN-Lisp creators, including Deutsch, moved to <a href=\"https:\/\/en.wikipedia.org\/wiki\/PARC_(company)\">Xerox PARC<\/a>, BBN-Lisp became <a href=\"http:\/\/www.softwarepreservation.org\/projects\/LISP\/interlisp_family#INTERLISP_\">INTERLISP<\/a>. By this time, Deutsch had received his bachelor\u2019s 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.<\/p>\n<p>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 <a href=\"http:\/\/www.softwarepreservation.org\/projects\/verification\/pivot\/Deutsch-Pivot.pdf\/view\">listing<\/a> and his <a href=\"http:\/\/www.softwarepreservation.org\/projects\/verification\/pivot\/Deutsch-An_Interactive_Theorem_Prover-1973.pdf\/view\">thesis<\/a> to be posted on the SPG web site.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>PIVOT, the program verification system written in BBN-Lisp by L. Peter Deutsch and described in his PhD thesis, &#8220;An interactive program verifier&#8221; 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, &hellip; <a href=\"https:\/\/mcjones.org\/dustydecks\/archives\/2015\/05\/14\/810\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;L. Peter Deutsch&#8217;s PIVOT program verification system&#8221;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[10,20],"tags":[],"class_list":["post-810","post","type-post","status-publish","format-standard","hentry","category-lisp","category-program-verification"],"_links":{"self":[{"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/posts\/810","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/comments?post=810"}],"version-history":[{"count":18,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/posts\/810\/revisions"}],"predecessor-version":[{"id":830,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/posts\/810\/revisions\/830"}],"wp:attachment":[{"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/media?parent=810"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/categories?post=810"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mcjones.org\/dustydecks\/wp-json\/wp\/v2\/tags?post=810"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}