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
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
