> 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

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