The de Bruijn criterion is an "architectural" principle that is used in software that implements logic, e.g. proof assistants.
Logics are usually implemented in the interest of formal proof: we implement a logic precisely because we want to formally check that a mathematical theorem holds. Suppose indeed that our implementation says that a theorem does hold. If the logic is consistent, and our software correctly implements the logic, then the answer is probably yes. But how can we be sure that we have implemented the logic correctly?
The de Bruijn criterion is one approach to this problem. An implementation of a formal system satisfies the de Bruijn criterion exactly when the generation of the proof (i.e. the part of our software that helps us construct the proof) and the checking of the proof (i.e. the part of our software that checks whether a proof is correct) are independent.
The criterion is described as follows by [Barendregt and Wiedijk 2005]:
One may wonder whether proofs verified by a computer are at all reliable. Indeed, many computer programs are faulty. 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.
The de Bruijn criterion is satisfied by the Coq proof assistant.
According to Larry Paulson [2022], it was also satisfied by Robin Milner's Stanford LCF.
An alternative to satisfying de Bruijn criterion is the architecture used by LCF-style theorem provers, which was the main architecture of Edinburgh LCF and its many successors.
History question: when is the earliest description of the de Bruijn criterion in the literature?
A discussion of the de Bruijn criterion appears in a January 2022 blog post by Larry Paulson
The description given above originates in
Barendregt Henk and Wiedijk Freek 2005. The challenge of computer mathematics. Philosophical Transactions of the Royal Society A. 363: 2351–2375. http://doi.org/10.1098/rsta.2005.1650