Re: [Hol-info] verifying the Gordon computer
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 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
Re: [Hol-info] verifying the Gordon computer
I take it there's nothing in the CL area that used to be something like /usr/groups/hvg ? Michael On 2/4/18, 08:41, "Konrad Slind" wrote: 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 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 -- 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
Re: [Hol-info] verifying the Gordon computer
On 2 Apr 2018, at 10:47, wrote: > > I take it there's nothing in the CL area that used to be something like > /usr/groups/hvg ? I couldn't find it, though it may simply have moved somewhere. More worrying is that none of the older links on this page work anymore: http://www.cl.cam.ac.uk/research/hvg/HOL/ The source files of HOL88 are online here: https://doi.org/10.17863/CAM.10246 I downloaded them in the hope that this example would be included, but sadly not. It would be great if somebody could get their hands on some version of this proof! 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
Re: [Hol-info] verifying the Gordon computer
Hi, I didn't follow the entire discussions about “Gordon computer”, but if you just want to run HOL88, that’s easy. All you need to do is an Ubuntu 16.04 Linux environment (or Debian GNU/Linux), and install the “hol88” (and other hol88-*) packages [1, 2]. Latest version is “2.02.19940316”. Building HOL88 from scratch with original source files requires some basic Lisp skills, because you need a working GNU Common Lisp (GCL) to build a Classic ML, then use Classic ML to build HOL88. Hope this helps, Chun [1] https://packages.debian.org/search?keywords=hol88 [2] https://packages.ubuntu.com/search?keywords=hol88 > Il giorno 03 apr 2018, alle ore 13:24, Lawrence Paulson ha > scritto: > > On 2 Apr 2018, at 10:47, > wrote: >> >> I take it there's nothing in the CL area that used to be something like >> /usr/groups/hvg ? > > I couldn't find it, though it may simply have moved somewhere. More worrying > is that none of the older links on this page work anymore: > > http://www.cl.cam.ac.uk/research/hvg/HOL/ > > The source files of HOL88 are online here: https://doi.org/10.17863/CAM.10246 > > I downloaded them in the hope that this example would be included, but sadly > not. It would be great if somebody could get their hands on some version of > this proof! > > 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 signature.asc Description: Message signed with OpenPGP -- 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
Re: [Hol-info] verifying the Gordon computer
Thanks for your kind answer, but I'm really looking for the opposite: to run the classic old examples using the latest technology. It's a way of measuring the progress of our field. Larry > On 4 Apr 2018, at 21:59, Chun Tian wrote: > > Hi, > > I didn't follow the entire discussions about “Gordon computer”, but if you > just want to run HOL88, that’s easy. > > All you need to do is an Ubuntu 16.04 Linux environment (or Debian > GNU/Linux), and install the “hol88” (and other hol88-*) packages [1, 2]. > Latest version is “2.02.19940316”. > > Building HOL88 from scratch with original source files requires some basic > Lisp skills, because you need a working GNU Common Lisp (GCL) to build a > Classic ML, then use Classic ML to build HOL88. > > Hope this helps, > > Chun signature.asc Description: Message signed with OpenPGP -- 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