IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Bates's Point: Words could matter to programs too, though.
Even if appearance of expressions and naming are not normally considered essential to formal correctness, this, as pointed out to me by Joe Bates, does
not mean they could matter only to humans or be purely informal. It could well be that some heuristics for performing inference could indeed make use of how expressions look and how things are named. Still, such data can be supplied to these programs without building them into the formal material directly. Indeed, we intend for specifications of how to display expressions and how to denominate entities to be themselves expressed as texts to be included as objects in the FDL, and they would therefore be made available to such proof heuristics as needed.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html