This means that we are not obliged to create methods for content creation generally, but must flexibly anticipate likely methods, including extant ones, and publish adequate methods to access and contribute to FDL collections. Because of the variety of semantical intentions and epistemic assumptions, sometimes incompatible, underlying different developments, flexible and stringent accounting methods must be introduced if these mixtures of content are to coexist.
What we offer are to-some-extent common syntactic structures, storage, and accounting services, especially accounting for formal facts contributing to arguments for validity of proofs. See the glossary entries for
Further, we shall not require a particular logic (even a particular form of assertion), type theory, tactics, or the use of the ML programming language. However, it should be noted that our experience with these has led us to reject a number of presumptions about methods of proof and expression and left us with an expectation of rather liberal practices. In particular, we have become accustomed to using a language in which, as in informal mathematical practice, the sensibleness of expressions is not always obvious, and must sometimes be demonstrated, and in which some other simplifying assumptions about notational adequacy are avoided (such as assuming there is a single domain of all values). Our use of tactics to formalize the notion of effectively explaining how to make inferences, rather than restricting our expression of inference to schematic forms, has forced us to deal with issues pertaining to accounting for reliability of programs. Briefly, we have already committed ourselves to, and are experienced with, sophisticated methods of applied logic, and are therefore more likely than we would otherwise be to anticipate a great variety of formal methods.
A major purpose for development of our newest system is to analyze many concerns about how to simultaneously support independent developments. Many of these concerns were driven by centrifugal forces within our own project, whose members represent a variety of different opinions about how to formulate and develop formal mathematics, sometimes differing even as to what is legitimate. Our desire despite this to share what we can in various ways has driven us to a flexible design.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html