Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Formal Artifacts and Informal Understanding.

By the "formal" we mean that which has precise meaning or objective, ideally computer verifiable, criteria of correctness, based upon the "syntactic" form of the content. By the informal we simply mean everything else. An informal practice or artifact may have formal components.

We consider it essential to embed formal Texts (proofs, programs, definitions, propositions) in a body of informal Texts, recognizing that the use of the formal material is in any case embedded in informal practices.

If the formal artifacts are completely separated one will not understand how to apply them. Often these artifacts are formalized counterparts to informal ones. Some benefits of formality are that analysis can be pursued to great detail, and that combinations and transformations of the formal artifacts can often be performed mechanically without need for human intervention in order to make sure the particular intermediate stages of manipulation are meaningful and correct; systematic and abstract arguments about formal expression can be made reliably (sometimes such argument can itself be made formally by reflective devices).

Formalization should be introduced where it is economical to do so. A smooth flow and intricate interweaving between the formal and the informal is key to correctly deploying formal artifacts.

Complementary to introducing formal artifacts in place of informal material is attaching informal material to formal artifacts in order to better expose them to human understanding, much of which is not in fact formalized. It should be further noted that informal material can be formalized in various ways, and that the same formal material can be variously organized informally. Thus many interwoven organizations are natural. See Words vs Formality and see Readings. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes