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
)