On 02/09/17 18:05, Chun Tian (binghe) wrote: > 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.
Thanks for your reply. I understand your point. I had an impression which is in agreement with your commentary: I know very little of SML and OCaml to make an overall comparison. But I know that a point where SML easily beats OCaml is that SML has a clear and formal specification and is a stable language with many implementations, very much like C or Common Lisp. On the other hand, OCaml appears to change frequently and it is implementation-centered like Python instead of specification-centered. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
