4 ms·

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 s

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".
- deleted 8y ago
  [deleted]

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".

deleted 8y ago
[deleted]