Re: [mizar] PVS GPLed

[Freek Wiedijk <freek@cs.ru.nl>]

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