Hi John and Makarius, This is not very much about HOL as such, so if this reply is inappropriate for the HOL list, I apologise:
>>mutating the names of constants. I always found this "mutable constants" complaint silly. Many people make it, but it never struck me as significant. Surely in every practical programming language you can "cheat" in some way if you try hard enough. For instance by poking the memory, either internally through some Obj.magic like interface, or if you don't get that from your language by poking in /dev/mem? So the possibility of cheating if you really try does not seem an interesting one to me. What's important is that you won't "cheat" accidentally, by misunderstanding how things work. For example there is the story of someone who thought that some system had a superefficient automated prover, which made him super excited. Only later he found out that that "automation" had been the system's equivalent of what in HOL Light is called CHEAT_TAC (adding the thing to be proved as an axiom.) >In particular, one can generate a proof trace and check >it in a specially designed system like HOL Zero or even >write one's own proof checker. This certainly applies >to HOL Light and Isabelle, with Coq a more arguable >case. (Although it has a small kernel, this involves a >quite complex evaluation mechanism.) I think Matita started its life that way? So about Coq having a small kernel: I seem to remember that the source of Coq's latest kernel is larger than the source of the full Mizar system. Also, I always think that the _full_ "logic" of Coq (the thing called "pCIC") has nowhere been precisely written down. If I'm wrong about that, I _very_ much would like to know. (I know about the Coq manual, but that certainly is not the full story, nor is it written in a very precise style.) Freek ------------------------------------------------------------------------------ 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
