The proofs might still run. I'd be keen to help get them going, if they can be dug up. After Tamarack, Brian Graham verified a hardware-level SECD machine while a student of Graham Birtwistle. Perhaps they have running versions of those proofs.
Konrad On Sun, Apr 1, 2018 at 4:39 AM, Lawrence Paulson <l...@cam.ac.uk> wrote: > In 1983, using LCF_LSM, Mike verified his computer with the comment “The > entire specification and verification described here took several months, but > this includes some extending and debugging of LCF_LSM … it would take me two > to four weeks to do another similar exercise now. The complete proof requires > several hours CPU time on a 2 megabyte Vax/750.” > > Jeff Joyce verified several versions of this computer (which he called > Tamarack) using HOL. Do any of these proofs still run? I wonder how long it > takes now? > > Larry > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
