Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hello Jeremy. Thanks for your reply. On 05/10/17 13:25, Jeremy Dawson wrote: > Hi Mario, > > I don't mind the question, but the answer may not be much use because > it's a comparison between the 2005 version of Isabelle which I use and > HOL4. > > In terms of the type systems they are

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Jeremy, >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. In Coq and Mizar I don't have this experience, in the sense that I hardly ever need

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

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

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Chun Tian, I don't know much about rich(er) type systems, and I'm not well acquainted with Coq, but I'd say that what can be done in Isabelle or HOL should be possible also in richer type systems. Regarding modelling of a proof, the context of what I said is describing, in HOL or

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

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

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

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

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Mario, I don't mind the question, but the answer may not be much use because it's a comparison between the 2005 version of Isabelle which I use and HOL4. In terms of the type systems they are identical. Isabelle has schematic variables and type classes, both of which can make proof

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

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

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Ramana, >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.) One can do everything with anything. So dependent tpes certainly are not _needed_ for

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

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.) On 15 September 2017 at 11:06, Mario Castelán Castro wrote: > Hello. > > I

[Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hello. I want ask for your experience and opinion of proof assistants with “rich” type systems (allowing types dependent on terms and “proofs as terms, propositions as types”) like Agda and Coq. Specifically, how practical are these systems for pure mathematics, compared to HOL4 and HOL Light? Is