On 05/10/17 11:53, Jeremy Dawson wrote: > Hi Mario, > > Slightly off-topic, I had experience with the type system of HOL-Omega > (system F, if I recall the terminology right, not dependent types, so my > experience may not be very relevant) > > My dominant recollection is the difficulty of getting the system to do > the right type inference, and getting terms to typecheck. I was forever > working out where I needed to put in type annotations. Quite > frustrating after my experience with regular HOL, and Isabelle. > > It led me to conclude that the systems offering automatic inference of a > principal type really occupy a "sweet spot", ie the best compromise > between ease of use and expressive power.
Hello Jeremy. Thanks for your answer! If you do not mind an off-topic question, what differences in terms of usability and ease of formalizing pure mathematics did you experience find between Isabelle and HOL4 (or HOL Light if that is the one you use)?. -- 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
