6
$\begingroup$

Background: definition of de Bruijn Criterion. Henk Barendregt coined the term "the de Bruijn criterion", which seems variously defined as:

It was emphasised by de Bruijn that in case of verification of formal proofs, there is an essential gain in reliability. Indeed a verifying program only needs to see whether in the putative proof the small number of logical rules are always observed. Although the proof may have the size of several Megabytes, the verifying program can be small. This program then can be inspected in the usual way by a mathematician or logician. If someone does not believe the statement that a proof has been verified, one can do independent checking by a trusted proof-checking program. In order to do this one does need formal proofs of the statements. A Mathematical Assistant satisfying the possibility of independent checking by a small program is said to satisfy the de Bruijn criterion.

Bluntly, I would posit "having a sufficiently small kernel" suffices to satisfy the de Bruijn criteria.

Question

How many lines of code qualify as "sufficiently small kernel"? For what values of $N$ will having "$N$ lines of code" be "too big"?

Attempted solution

It's impossible to have "absolute certainty" a program is bug free. But we can estimate the probability it's bug free.

The industry standard has been the number of bugs per thousand lines of code is

$$\rho=20/1000. \tag{1}$$

This could be used as an estimate for the probability $p_{\text{bug}}$ a given line of code is buggy.

Using a binomial distributed random variable for the number of bugs $B\sim\mathrm{Bin}(N,p_{\text{bug}})$ and Chebyshev's inequalities to approximate $\alpha=0.05$ significance as $B$ being within $3\sigma$ of zero, then $\Pr(B\leq 3\sigma\mid N,p_{\text{bug}})\geq 0.5$ would give us $N\approx 533$ lines of code.

Remarks. (1) Curiously, only HOL Light would qualify as probably satisfying the de Bruijn criterion.

[Addendum: it appears that a few Metamath checkers probably satisfy the de Bruijn criterion as well, e.g., mmverify.py (350 lines of python), mmamm.m (74 lines of mathematica), hmm (400 lines of haskell). H/t Mario Carneiro. It further appears that Isabelle probably satisfies the de Bruijn criterion, its "nanokernel" Pure/context.ML is 512 lines of Standard ML code as of git commit cee2c40.]

(2) This is a little too "handwavy" for my comfort, but it gives a heuristic neighborhood answer. Another derivation using the negative binomial distribution would give $N\approx 411$ lines of code, for example.

(3) Presumably different programming languages and different programming practices affect the value of $p_{\text{bug}}$, and I'm certain there's some Bayesian way to further improve the situation. But I don't think this would change things more than a hundred lines of code, or so.

Addendum (4) It seems that the following probably fail to satisfy the de Bruijn Criterion:

  • Lean 4 (kernel is 5875 lines of code as of git commit 340c331da9)
  • Coq (kernel is 27514 lines of code as of git commit d8393d7)
$\endgroup$
6
  • 4
    $\begingroup$ What if the kernel code is proven to be correct by another proof assistant? $\endgroup$ Feb 10, 2022 at 5:13
  • 2
    $\begingroup$ Some of Metamath's third party verifiers deserve a mention: mmverify.py (350 lines of python), mmamm.m (74 lines of mathematica), hmm (400 lines of haskell). A metamath verifier was even adapted to improve on the state of the art smallest unprovably halting turing machine: the NQL compiler was used to build a 1919-state TM enumerating ZF theorems looking for False. $\endgroup$ Feb 10, 2022 at 9:02
  • $\begingroup$ @MarioCarneiro Wonderful! I was unaware of these examples, though NQL kinda straddles the domain of applicability for the de Bruijn criterion (in my mind, at least). $\endgroup$ Feb 10, 2022 at 16:58
  • 2
    $\begingroup$ Of course even a formalized proof of something doesn't give "absolute certainty", but it drastically reduces the probability of the existence of bugs. If proof assistant A formalizes a proof of the correctness of the kernel of proof assistant B, then what you have to calculate is the probability not just that A has a bug, but that that bug is of the sort to cause it to mistakenly accept an incorrect proof of the correctness of B. Most bugs could not have such an effect even in principle, and those that could are very difficult to exploit accidentally. $\endgroup$ Feb 10, 2022 at 18:31
  • 1
    $\begingroup$ Mike is probably suggesting something like the "hereditary de Bruijn criterion" ;P $\endgroup$
    – Trebor
    Feb 13, 2022 at 5:17

1 Answer 1

6
$\begingroup$

Do you have a source for the probability of 20 bugs for 1000 lines you give? In particular, at which stage of development does this apply?

The reason I ask this is that indeed at the first iteration of development a proof assistant kernel might fall into your setting. But kernels are usually quite stable and scrutinized/tested by a lot of people, so that bugs are detected (and corrected) over time. Thus, the older and the more used a proof assistant is, the less likely it is that a bug has stayed undetected this whole time. Usually, when such a bug is found, it’s in the new, experimental features rather than in the old, well-tested ones.

Therefore, I would have more trust in (the non-experimental) parts of e.g. Agda’s kernel, even if it’s quite large, than in a brand new proof assistant no one has used yet, even with a very small kernel.

$\endgroup$
2
  • 1
    $\begingroup$ The "20 bugs per 1000 lines of code" is industry folklore. I can dig out the studies underlying it, but I think it's a shifting standard (study A says 23 bugs per kloc, study B says it's 18, etc.). Further, it probably varies according to language used, programming practices employed, etc. The $\rho=20/1000$ seems like a fine upper bound on the "probability of bugs", and gives a lower bound on the number of lines of code. $\endgroup$ Feb 10, 2022 at 19:15
  • $\begingroup$ (Also, I'm sorry for the belated comment, I wrote a version of this earlier, but apparently didn't post it? That's what happens when I do stuff before having my morning coffee...) $\endgroup$ Feb 10, 2022 at 19:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.