|FDL||- Formal Digital Library; a repository of a certain kind with a process for using it ;|
We imagine a Formal Digital Library as a repository for formally verified material along with other complementary material, much of which is essential for practical use of the formal. The complementary material is either unverified, only partially verified, or perhaps not subject to verification by machines. Further, we conceive of the FDL as a
Actually we usually mean here an architecture suitable as a basis for building such libraries, and use the term (the "L" part anyway) with some reservations, but it continually indicates one of our main intentions.
One should expect that
Among the content of an FDL are specifications for how to verify formal content. It is not part of the FDL design to govern what counts as legitimate validation, and indeed FDLs are intended to be radically open. This requires accounting for what has been verified and by what means.
Different implementations of FDLs are possible and expected, and they may provide different services beyond the minimal, as well as have their own policies for access and contribution.