Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Makarius <mak...@sk...>]

On Wed, 25 Apr 2012, Bill Richter wrote:

> Makarius, I (following Freek) tend to think that Isabelle might be the 
> best language for high school teaching axiomatic proofs, but Isabelle is 
> intimidating, lots of programs to install & lots of dox.

Some agreements and disagreements here:

  * High-school teaching: I don't think we are there yet.  Yes for certain
    university courses, say for logic, programming language semantics, and
    a bit more.

  * Intimidating Isabelle architecture: depends.  Do you find a Gothic
    Cathedral intimidating?  It is not something you build at home in your
    spare time, though.

  * Lots of programs to install: definitely not.  It is basically one piece
    of download with everything included, hardly any installation at all.
    Same for Coq, mostly.  I think it is a trait of the original HOL
    community to insist in the build-it-yourself-from-scratch model.

  * Isabelle documentation: diverse, potentially confusing, too many
    manuals.


 	Makarius