On Fri, 27 Apr 2012, Paul Graunke wrote:
> 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.
Yes, that is an important point. When I get on a train, I buy a train
ticket, not the technical manuals to take it apart and rebuild it myself
again. Or when I want to run an operating system I download Ubuntu and
spend maybe 30min with a few trivial clicks to get it working by itself.
No need to understand X11 server configuration anymore, what that was
commonplace 10 years ago.
Nonetheless, as I've said earlier on this thread, the different provers do
have their own cultural traditions, and these are one of the reasons to
have such a diversity. I occasionally sit down with a student and take
HOL-Light apart and re-assemble it in a few hours. It helps to get some
understanding of the bare-bones things, and also of the complex
infrastructure that systems like Coq or Isabelle put around the raw
material.
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
