- The gap between formal and informal has been pointed out as an Achilles' heel of formal methods from the dawn of the field, so critique is not particularly new. The standard reference is Social processes and proofs of theorems and programs (1979), which is worth reading.
- Nice; thanks for the pointer to the paper (i had not known of it).
The key to understanding and usage of Formal Methods is to realize that it is a way of thinking at many different levels. You can choose whatever level seems intuitive and accessible to you.
The must-read paper On Formal Methods Thinking in Computer Science Education posits three levels which i have highlighted here - https://news.ycombinator.com/item?id=46298961
Carroll Morgan's classic (In-)Formal Methods: The Lost Art --- A Users’ Manual and his recent book on the same are also relevant here - https://news.ycombinator.com/item?id=45490017
- the author seems unaware of the SAT/SMT solver/analysis ecosystem
- "Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something."
- Why do you think so? I didn't get such impression.
