Hi Makarius, | A system like HOL-Light has the advantage that the reader gets quickly an | impression what the basic logic functionality is meant to be. This gives | some certainty under additional assumptions, i.e. that the ML really is | what it seems at first sight, and that certain bad things are not done in | practice. (Say someone taking apart terms and mutating the names of | constants.)
That is true. I actually had in mind not so much a practical metric of ultimate certainty, but more the conceptual feeling that you completely understand in principle what's going on when you prove a theorem and know and trust the underlying logical rules. The question of providing ultimate assurance is a bit different, but I think any system with a small kernel of simple logical steps provides a relatively easy path to such certainty for those that care enough. 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.) | Driving this further and further, adding infrastructure to address | weaknesses of the implementation and other side-conditions, you get to a | highly complex system like Isabelle. Here the idea is to provide a secure | and fast environment to the end-user, like an operating system does, but | the first impression that one could easily understand it is lost. Yes, I think the two approaches are nicely complementary and probably appeal to different people. So there is room for both styles. John. ------------------------------------------------------------------------------ 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
