Our project is especially interested in the certification of formal proofs according to specific (user suppliable) criteria, and when stressing this function, when thinking of the FDL services as principally directed at supporting this function, we call it a "logical library". A particularly esteemed feature a certificate may exhibit is its making an objective and independently verifiable claim; this is the ideal for "logical" claims, and is the alternative to authority. Of course, one might view this as the essence of scientific claims generally, but the procedures for verifying "logical" claims are largely reducible to automatic methods which are in principle directly verifiable by an automated text management process since it can itself in principle perform, and so certify, the computations.
One aspect of ordinary libraries we emulate is theoretical neutrality. Thus, we do not require that ordinary documents must be "correct", indeed there is no privileged criterion for correctness of ordinary texts. Criteria for correctness (via proof engines, eg) are supplied by the users of the FDL as contributions to the text collection.
Certificates in the FDL, however, are guaranteed to be correct according to published criteria; the criteria for certificate correctness must therefore be understandable to users of the "logical library". The correctness of some certificates will be independently verifiable, the ideal for logical claims, but other certificates may not be practically verifiable because they attest to the existence of something that is not made practically accessible (an example being a certificate meaning that there once was a proof of a given formula in the collection).
When a process, say with a user behind it, accesses a collection, the "view" is a sub-collection of objects we call the
This leads us to the matter of