In order to formalize things, we need to push all the informality together into “undetermined words”. The standard examples are Euclidean “line” and “point”. It’s entirely possible to do proof theory and to write proofs entirely as a game of symbols. We do not need to pronounce the mountain /\ as “and”, nor the valley \/ as “or”. A formal system doesn’t need to be interpreted.
Your sentence “Surprisingly, the MEANING of formal symbols is still in most cases reduced to informal words like “or” and “and” somewhere down the road.” seems to hint at something like “Surprisingly, formal symbols are FUNDAMENTALLY based on informal notions.” or “Surprisingly, formal symbols are COMPRISED OF informal notions.”—I will vigorously oppose these implications.
We step from the real world things that we value (e.g. stepper motors not banging into things) into a formal system, interpreting it (e.g. a formal specification for correct motion). (Note: formalization is never protected by the arguments regarding the formal system’s correctness.) After formal manipulations (e.g. some sort of refinement calculus), we step outward again from a formal conclusion to an informal conclusion (e.g. a conviction that THIS time, my code will not crash the stepper motors). (Note: this last step is also an unprotected step).
In order to formalize things, we need to push all the informality together into “undetermined words”. The standard examples are Euclidean “line” and “point”. It’s entirely possible to do proof theory and to write proofs entirely as a game of symbols. We do not need to pronounce the mountain /\ as “and”, nor the valley \/ as “or”. A formal system doesn’t need to be interpreted.
Your sentence “Surprisingly, the MEANING of formal symbols is still in most cases reduced to informal words like “or” and “and” somewhere down the road.” seems to hint at something like “Surprisingly, formal symbols are FUNDAMENTALLY based on informal notions.” or “Surprisingly, formal symbols are COMPRISED OF informal notions.”—I will vigorously oppose these implications.
We step from the real world things that we value (e.g. stepper motors not banging into things) into a formal system, interpreting it (e.g. a formal specification for correct motion). (Note: formalization is never protected by the arguments regarding the formal system’s correctness.) After formal manipulations (e.g. some sort of refinement calculus), we step outward again from a formal conclusion to an informal conclusion (e.g. a conviction that THIS time, my code will not crash the stepper motors). (Note: this last step is also an unprotected step).