My highly subjective opinions: as an end-user, I choose HOL4 over HOL light because I think and/or found:
1. Standard ML is a better language than OCaml (as a programming language); 2. Poly/ML is a better implementation than OCaml (as a language implementation); 3. HOL4 has a richer and more systematic theory library. The logic core of HOL family of theorem provers is already much simpler than others (e.g. Coq). Although the logic core of HOL light sounds more reasonable and slightly simpler, the fact that it’s implemented in OCaml and it lacks of many useful theories which I depend on, has lead me to stick with HOL4 and ignore HOL light. But I admit, as theorem provers they’re equally powerful, given both infinite time, I can’t imagine any formalization project which can only be done in one of the two software. —Chun > Il giorno 02 set 2017, alle ore 21:40, Mario Castelán Castro > <marioxcc...@yandex.com> ha scritto: > > On 01/09/17 15:12, Ken Kubota wrote: >> Hi Mario, >> >> John has explained some of his motivation for HOL Light in an email >> available online at […] > > Thanks you. These links provide useful insight. > >> A HOL family tree with both HOL4 and HOL Light can be found at […] and at >> […]. > > Yes, I have read those papers. But they focus mostly on the foundational > and not the user-level differences. > >> What makes HOL Light special (in my opinion), is that it tries to >> reduce the logic to a simpler logical core (hence, HOL "Light"). >> In this respect, it is very similar to the philosophy of Metamath and Q0/R0. >> >> For this reason, I chose HOL Light as point of reference in my draft >> describing R0, writing that "HOL Light […] has [only] 'ten primitive >> rules of inference' [Harrison, 2009, p. 61]" [Kubota, 2015, p. 14]. > > I see. It is good to know. But these differences are abstracted from the > user who writes proofs using high-level tactics. I doubt that even at > the level of applying inferences to the theorem data type through the > OCaml or ML interface, it would make much difference whether –for > example, “SUBST”– is primitive or derived. > > From the level of writing high-level proof scripts, is there any > difference between the systems, apart from the choice of > metalanguage/programming language (SML and OCaml) and the differences in > the name of the identifiers of tactics? > >> Recalling our previous private communication, I could send you >> the draft describing R0, if you are interested (for private use only, >> please do not quote). I hope to publish a full description by the >> end of the year. > > I thank you for your kindness and confidence. > > I am still studying the “well-known” formal systems of type theory. I > have read chapter 1 of HOL4's “The HOL system LOGIC [For HOL > Kananaskis-11]” and I am currently reading “Type Theory and Formal > Proof: An Introduction” by R. Nederpelt and H. Geuvers (2014). > > Thus although I am interested, I shall turn down your kind offer because > –right now– my background knowledge in type theory is very limited, and > could neither make much use of the draft nor provide the feedback that > is expected when sharing pre-publication drafts. I am fine waiting until > your paper is ready as I have much to read of the same topic in the > meantime. ☺ > > ----- > Regards. > > -- > Do not eat animals; respect them as you respect people. > https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan > > ------------------------------------------------------------------------------ > 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 using GPGMail
------------------------------------------------------------------------------ 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
