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
