Library, Archival, and Workspace Functions

The intention that the FDL be oriented towards the maintenance of Formal materials, particularly charged with maintaining verified relations between formal documents such as logical relations between digital documents and artifacts, compels us to maintain records in the manner of archives (in the sense of archival science). The point of formal entities is that there are explicit verifiable criteria for claims about them and relating them, and much of their value depends on establishing and recording the validation of such claims; these are essentially archival functions.

A library of Formal documents maintained in isolation without regard to their relations between each other or without regard to whether the verifiable relations claimed for them actually obtain, is considerably less useful than one which maintains records of these verifications. Thus, we would consider the archival functions to be essential to any Formal Digital Library. And complementarily, we consider the inclusion of informal material essential to any large body of formal material to make it widely and repeatedly useful (see Formal vs Informal).

Workspace is a different matter, though. Functions supporting the development of material for eventual submission to an FDL are not essential for the use of the FDL as a repository of information and knowledge. Indeed, the needs of a person or organization or community trying to develop material may be significantly greater than those who simply need to access it, and implementation of a workspace facilitating experimental development and collaboration may go significantly beyond effective implementation of a digital repository. Thus, we would not expect every FDL to effectively support development.

However, because of the record-keeping functions of the FDL, effective development of material that will meet the certification requirements implicit in the useful submission to an FDL, effective development of formal material to be submitted requires that the material be developed incorporating the same record-keeping devices as are needed in the target repository. Archival scientists have articulated essentially the same principle by holding that the original record creating institution needs to adopt record creation methods that anticipate archiving.

This suggests that although not every FDL needs to efficiently implement workspace functions, it is important that appropriate workspace processes be implemented. Our FDL design includes workspace functionality, since the same basic accounting devices should be used for the repository and development. Different FDLs may be maintained and differently implemented with varying emphases on facilitating workspace functions.

One institution might implement an FDL principally for "publication" of formal material with little support for development. Perhaps this FDL provides utilities to expedite search and establishes policies for long retention, but does not allow modification of submitted material, or provide development oriented facilities such as multiplexing Inference Engines for heuristic proof methods. Another organization may implement relatively low storage capacity FDLs aimed more at development of material to be submitted later to other FDLs, and may emphasize version control and flexible methods for collaboration between developers.

Finally, it should be noted that the design of "finding aids" is not an explicit part of the FDL design, and yet without such facilities for finding content in a repository one can hardly consider the collection to be a library or an archives. Finding aids are essential, but we consider them to be content themselves; methods of organizing and finding content are themselves contributions that can be accessed, innovated and improved upon. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html