12 ms·

The meaning of 'formal' really depends on the context and is a matter of degree. This is readily apparent from your identification of formal with mechanical. T

The meaning of 'formal' really depends on the context and is a matter of degree. This is readily apparent from your identification of formal with mechanical. That immediately forces the question: which machine? > a formal description is one that could be directly mechanically interpreted by a simple computer program as written Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal. If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'

pron 8y ago
> The meaning of 'formal' really depends on the context Yes, I say, "in the context of proofs." > That immediately forces the question: which machine? From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical. > Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better. > If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof. > the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal. See https://en.wikipedia.org/wiki/Logic#Logical_form https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form https://en.wikipedia.org/wiki/Logical_form > 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?' I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.
- abecedarius 8y ago
  I like to say 'semiformal' of arguments meant for humans which could also be turned into a formal argument without calling on too much cleverness. (That's of course a matter of opinion or judgement.) Like pseudocode for programs.
- smallnamespace 8y ago
  If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement? Note that 'formal' has another common definition in the context of software engineering: https://en.wikipedia.org/wiki/Formal_methods#Taxonomy https://en.wikipedia.org/wiki/Formal_methods#Taxonomy I like this definition because it explicitly shows formal is really a continuum—since in the limit, you should go all the way down to ZF, but in practice nobody actually does this. A hard, black-and-white definition for formal is simply less useful. It seems that your objection can be summarized as: 'formally prove' has only a single meaning in the context of a proof, the mathematical one. IMHO is uncharitable to the author, since there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
  - pron 8y ago
    > If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement? Not really, because he doesn't formalize the problem (i.e. write it in a formal system). But I may not have commented if the term "formal" wasn't so emphasized and used so often. This emphasis and repetition means that people simply don't know what formal means, and so I thought it was an opportunity to point out this rather common mistake. > Note that 'formal' has another common definition in the context of software engineering It's the very same definition. At all levels, the word "formal" actually means formal -- i.e., stated in a formal language. > but in practice nobody actually does this. 100% of whatever it is that you do in formal methods is actually formal. You don't necessarily need a deductive formal proof, but in order to say formal you need to be formal. Static analyzers are 100% formal, as are model checkers. Even tests are 100% formal (although they don't fall under the umbrella term "formal verification" for unrelated reasons). > there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering. Not to my knowledge. I am not aware of any use of "formal" in the context of logic, proofs, computer science or software where it does not mean "mechanical".

pron 8y ago

> The meaning of 'formal' really depends on the context Yes, I say, "in the context of proofs." > That immediately forces the question: which machine? From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical. > Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better. > If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof. > the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal. See https://en.wikipedia.org/wiki/Logic#Logical_form https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form https://en.wikipedia.org/wiki/Logical_form > 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?' I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.

abecedarius 8y ago
I like to say 'semiformal' of arguments meant for humans which could also be turned into a formal argument without calling on too much cleverness. (That's of course a matter of opinion or judgement.) Like pseudocode for programs.
smallnamespace 8y ago
If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement? Note that 'formal' has another common definition in the context of software engineering: https://en.wikipedia.org/wiki/Formal_methods#Taxonomy https://en.wikipedia.org/wiki/Formal_methods#Taxonomy I like this definition because it explicitly shows formal is really a continuum—since in the limit, you should go all the way down to ZF, but in practice nobody actually does this. A hard, black-and-white definition for formal is simply less useful. It seems that your objection can be summarized as: 'formally prove' has only a single meaning in the context of a proof, the mathematical one. IMHO is uncharitable to the author, since there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
- pron 8y ago
  > If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement? Not really, because he doesn't formalize the problem (i.e. write it in a formal system). But I may not have commented if the term "formal" wasn't so emphasized and used so often. This emphasis and repetition means that people simply don't know what formal means, and so I thought it was an opportunity to point out this rather common mistake. > Note that 'formal' has another common definition in the context of software engineering It's the very same definition. At all levels, the word "formal" actually means formal -- i.e., stated in a formal language. > but in practice nobody actually does this. 100% of whatever it is that you do in formal methods is actually formal. You don't necessarily need a deductive formal proof, but in order to say formal you need to be formal. Static analyzers are 100% formal, as are model checkers. Even tests are 100% formal (although they don't fall under the umbrella term "formal verification" for unrelated reasons). > there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering. Not to my knowledge. I am not aware of any use of "formal" in the context of logic, proofs, computer science or software where it does not mean "mechanical".