On 04/26/2012 03:02 PM, Makarius wrote: > 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 > Yet the tutorial is a very nice place to start for documentation. =)
There is also a significant difference between learning to use a theorem prover vs taking one apart and putting one back together again. We use compilers and development environments to teach computer science without teaching how to build compiler or development environments until later typically. I argue that internal architectures are a separate issue from suitability for teaching. Paul ------------------------------------------------------------------------------ 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
