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

[Mario Castelán Castro]

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 identical.
> 
> Isabelle has schematic variables and type classes, both of which can
> make proof easier.  Otherwise, I don't find major differences.
> 
> Turning to modern day Isabelle - other factors may be:
> 
>   - the extent of unnecessarily incompatible changes between one version
> of Isabelle and the next (which is in fact why I'm still using the 2005
> version, when I'm not using HOL)
> 
>   - the difficulty of using ML to program complex proof tactics -
> mandatory for a small proportion of my work (I've had various and highly
> conflicting reports of whether this is possible or reasonably easy in
> current Isabelle)
> 
>   - documentation, and willingness of developers to help with questions
> (and for me, location at GMT+10 means I can often get an immediate answer)
> 
> In HOL4 the source code is effectively available for users to look at
> (in Isabelle they can look at it, but it - or a lot of it - is highly
> obfuscated).
> 
> Cheers,
> 
> Jeremy

-- 
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

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

[Freek Wiedijk]

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 type annotations where I don't expect
them.  In occasionally have problems with "match ... with
..." typing, getting that to work can be very frustrating.
But apart from that, I don't have much of a problem.

>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.

I don't mind so much explicitly typing my variables
where they are bound.  So I don't share this feeling of
Hindley-Milner style polymorphism being a "sweet spot".
I'd rather have full polymorphism and dependent types
as well.

Freek

--
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

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

[Mario Castelán Castro]

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

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

[Jeremy Dawson]

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 Isabelle, a proof system for some logic, and 
describing proofs in that proof system.


This is to be contrasted with an approach which I believe may be 
available in constructive logic systems, which is to do a proof in (say) 
Coq, then from that proof, to obtain a function which implements that 
proof, so in a sense you are getting an object representing the proof.


But I may be talking nonsense here, so you need the comments of someone 
more familiar with Coq or similar systems


Cheers,

Jeremy


On 06/10/17 05:38, Chun Tian (binghe) wrote:

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  
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




--
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

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

[Mario Castelán Castro]

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.

-- 
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

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

[Chun Tian (binghe)]

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 
>  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

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

[Jeremy Dawson]

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 easier.  Otherwise, I don't find major differences.


Turning to modern day Isabelle - other factors may be:

  - the extent of unnecessarily incompatible changes between one 
version of Isabelle and the next (which is in fact why I'm still using 
the 2005 version, when I'm not using HOL)


  - the difficulty of using ML to program complex proof tactics - 
mandatory for a small proportion of my work (I've had various and highly 
conflicting reports of whether this is possible or reasonably easy in 
current Isabelle)


  - documentation, and willingness of developers to help with questions 
(and for me, location at GMT+10 means I can often get an immediate answer)


In HOL4 the source code is effectively available for users to look at 
(in Isabelle they can look at it, but it - or a lot of it - is highly 
obfuscated).


Cheers,

Jeremy

On 06/10/17 04:49, Mario Castelán Castro wrote:

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)?.



--
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

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

[Jeremy Dawson]

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

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

[Freek Wiedijk]

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 formalization.  But dependent
types _are_ very convenient.  I know them both from Coq
and from Mizar.

In Mizar the foundations are untyped ZF-style set theory
(Josef Urban's PhD thesis is about cooking away all the
syntactic sugar), so you don't need an "an enormously
complex logic" (Mario's words) to get dependent types.

Examples of types that to me seem dependent in a natural
way are, in mathematics:

  element of the set X
  element of the carrier of the algebraic structure X
  vector space of dimension n
  normal subgroup of group G
  field of characteristic p
  field extension of field K
  simplicial k-complex
  morphism from A to B in a category

and in (theoretical) computer science:

  array of length n
  integer of signedness s and size n
  machine program of processor architecture P
  C program of implementation I
  normal form of term t under some reduction relation
  term of type A in a typed system

or in mathematical logic:

  proposition over a signature S
  proof of proposition A

Etcetera, etcetera.

The last actually _also_ has the signature S as an argument,
but it is "hidden" (implicit) because it can be inferred
from the type of A, so does not need to be written.
These implicit arguments are quite powerful.  For example,
when working in group theory, you can write x + y, but
actually it will be a ternary operation, with the group the
third argument that can be inferred from the type of x and y.

I know that John Harrison has a hack where he uses
type variables to simulate natural numbers, and you get
_something_ like dependent types in HOL that way.  But that
really only goes so far.

Now various of these types are sometimes in a natural way
empty (for example the type "normal form of term t", when t
does not have a normal form), which makes it so irritating
that Mizar doesn't allow for empty types.  Without dependent
arguments, not allowing for empty types is not a big deal
(like in HOL), but once you ahve dependent types you really
also have to allow for types being empty.

Even when you don't care at all (like I do, well maybe :-))
for the Curry-Howard isomorphism.

Freek

--
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

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

[Ramana Kumar]

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 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 there a significant advantage of these systems for pure
> mathematics compared to higher order logic?
>
> Systems with types dependent on terms promise many expressibility
> built-it into the logic. My impression is that this is unnecessary and
> generates more problems than what it solves. When one tries to make the
> logic as rich as possible instead of as simple as possible, containing
> everything that could be desired built-in, the result is an enormously
> complex logic (with the implications that the logical kernel, if any,
> will be more difficult to verify either by ordinary code review or
> formally). In the case of Coq, it is my understanding that the logical
> foundation even changes regularly with new releases.
>
> Yet a system that has everything that could be wanted from it is an
> unachievable goal. Users or interested parties eventually find something
> missing so a process of endless revision of the foundations begins.
>
> This does not seem to happen with foundations based on set theory. ZFC
> (possibly augmented with proper classes and large cardinals) seems to be
> both sufficient for all mathematics and written in stone (in the sense
> that we are not continuously revising the foundations continuously).
>
> What is thus the motivation for the search for logical foundations and
> systems based on “rich” type theory (beyond higher order logic)? Setting
> aside philosophical interest in type theories (intuitionism), is there
> some advantage to them as foundations or practical systems beyond the
> built-in syntactic sugar? I am missing something?
>
> Thanks.
>
> --
> 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
>
>
--
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

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

[Mario Castelán Castro]

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 there a significant advantage of these systems for pure
mathematics compared to higher order logic?

Systems with types dependent on terms promise many expressibility
built-it into the logic. My impression is that this is unnecessary and
generates more problems than what it solves. When one tries to make the
logic as rich as possible instead of as simple as possible, containing
everything that could be desired built-in, the result is an enormously
complex logic (with the implications that the logical kernel, if any,
will be more difficult to verify either by ordinary code review or
formally). In the case of Coq, it is my understanding that the logical
foundation even changes regularly with new releases.

Yet a system that has everything that could be wanted from it is an
unachievable goal. Users or interested parties eventually find something
missing so a process of endless revision of the foundations begins.

This does not seem to happen with foundations based on set theory. ZFC
(possibly augmented with proper classes and large cardinals) seems to be
both sufficient for all mathematics and written in stone (in the sense
that we are not continuously revising the foundations continuously).

What is thus the motivation for the search for logical foundations and
systems based on “rich” type theory (beyond higher order logic)? Setting
aside philosophical interest in type theories (intuitionism), is there
some advantage to them as foundations or practical systems beyond the
built-in syntactic sugar? I am missing something?

Thanks.

-- 
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