I like the "small kernel" approach of HOL Light (or was it already LCF?), and think that it is really very useful and "trust-encouraging". But I think it still requires quite some trust, assumptions, and knowledge about the implementation, when you say that thousands of additional lines of code "are safe" provided the small kernel is. There are other ways how to "raise trust" - independent code review by people/computers, independent proof review by people/computers, and I think this will always be empirical, regardless of the popular claims about having software "verified".
One particular problem I have with mathematics in HOL Light (and the same for Isabelle/HOL) is its set theory. I know that the hierarchy of sets is much "sparser" there (due to type constraints, you cannot have a set containing a real and an ordinal). I don't know what are its consequences e.g. for doing general topology based on this set theory. Note that e.g. the proof of Jordan in Mizar uses general topology (e.g. Urysohn's lemma). It seems to me that a lot of mathematicians assume the ZF framework, and I don't know how much are the consequences of limiting the universe thought through. Hopefully it's just my ignorance, and someone will enlighten me :-).
Josef On Tue, 16 Sep 2008, Freek Wiedijk wrote:
Josef:it is reality (and sometimes a nightmare) - all sufficiently complicated software is (sometimes) buggy.I've heard that a reasonable rate for commercial software is about two bugs per thousand lines of source code. I think that Mizar has about 80 thousand lines of source, so that means that it probably has between 100 and 200 bugs. Of course many of those won't be inconsistency bugs. At NASA with really important software they get the bug rate down to 0.2 bugs per thousand lines, I think, but that's really expensive! The HOL Light kernel is 669 lines. If we again use the figure of 2 bugs per thousand lines, that means that it might have 1.3 bugs. But once it's bug free, the mathematics that the system checks will be flawless! Won't that be nice? (Of course then there still might be problems introduced by the ocaml compiler, the OS, or the processor running the system.) Freek