On the other hand, our own abilities to understand formal material are often deeply tied to our habits of notation and nomenclature. Indeed they are so important that we must neither ignore these matters nor presume to be able to formalize them. Such habits may vary from person to person, from circumstance to circumstance, and from time to time. Often there is dispute over such choices of naming and notation, which need not impinge on the formalization process.
The use of abstract syntactic structure is widely understood to isolate structural features of notation pertinent to "formal" correctness. Of course there is a sense in which to write "3-4" to mean the result of subtracting three from four (instead of four from three), or to mean the sum instead of the difference, is wrong, but that is not a matter of formal correctness as intended here. When we employ formal notation in an informal context, such errors can be ruinous, and so we must have ways of avoiding them, but we take this to be a different issue from formal correctness.
Our project conceives formal structure, therefore, to be abstract. In particular we take the expressions or
Similarly, though written natural language is essential and should be included among, and intimately interwoven with, formal expression, we consider the meaning and syntax of natural language as a whole beyond the purview of the FDL project per se. As researchers succeed at formalizing parts of natural language, those parts may come to occupy more of the formal domain as those formal methods are introduced, but we must not depend upon that eventuality or put off the incorporation of informal language as mere uninterpreted text.
The independence of formal structure from notational appearance, epitomized by the use of abstract syntax trees instead of strings, eliminates much notational dispute from the formulation of formal expressions. But there remain the problems of resolving disputes and informal errors involving the names appearing as atomic components of formal structures. See