Hi Jeremy, I have a relevant question: one time we talked about the differences between Coq and HOL (thread title: "Difficulties when migrating proof scripts from Coq”), and you said:
"There's a distinction between an inductively defined set (in Isabelle or HOL) and a datatype, though they can look similar. I don't know which corresponds better to your Coq code You can model a proof by a proof tree "object" by using a datatype definition - then you have something of which you can define functions to give, eg, its' height, number of rule applications, etc.” Is the ability for theorem provers to do reasoning directly on “proofs” (or can we say “proofs” are 1st-class objects?) also a consequence of “rich” type systems? Regards, Chun Tian > Il giorno 05 ott 2017, alle ore 18:53, Jeremy Dawson > <jeremy.daw...@anu.edu.au> ha scritto: > > 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. > > Cheers, > > Jeremy Dawson > > On 06/10/17 03:46, Mario Castelán Castro wrote: >> On 04/10/17 20:09, Ramana Kumar wrote: >>> Perhaps it would make more sense to ask people who are using rich type >>> systems what their motivations are :) >>> (On this list it's probably mostly people who are satisfied with simple >>> type theory.) >> >> Yes, you are right. I wrote to this list because I am interesting in the >> opinion of informed “outsiders”, not only “insiders”, so to speak. >> >> >> >> ------------------------------------------------------------------------------ >> 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
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
