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
