# Probability and the de Bruijn Criterion

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)
• What if the kernel code is proven to be correct by another proof assistant? Feb 10, 2022 at 5:13
• 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. Feb 10, 2022 at 9:02
• @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). Feb 10, 2022 at 16:58
• 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. Feb 10, 2022 at 18:31
• Mike is probably suggesting something like the "hereditary de Bruijn criterion" ;P
– Trebor
Feb 13, 2022 at 5:17

• 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. Feb 10, 2022 at 19:15