4 ms·

My practitioner view of program analysis

49 points by evakhoury 6mo ago

sanxiyn 6mo ago
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.
- rramadass 6mo ago
  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 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 https://news.ycombinator.com/item?id=45490017
MWil 6mo ago
the author seems unaware of the SAT/SMT solver/analysis ecosystem
- sanxiyn 6mo ago
  Why do you think so? I didn't get such impression.
- dang 6mo ago
  "Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- jaen 6mo ago
  No. Did you even read the article? It talks about the "specification gap", which is the difference between the formalized semantics and the intended semantics. Every formal method has that problem (including the mentioned trivial ones like SAT and SMT).
jaen 6mo ago
There are ways to partially improve or at least quantify the specification gap using LLMs, by analyzing variance in the output formal specification when given a natural language specification (by eg. generating many formal specs from an input description). See eg. "Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning" [1]. [1]: https://arxiv.org/abs/2603.17233 https://arxiv.org/abs/2603.17233

49 points by evakhoury 6mo ago

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.

rramadass 6mo ago
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 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 https://news.ycombinator.com/item?id=45490017

MWil 6mo ago

the author seems unaware of the SAT/SMT solver/analysis ecosystem

sanxiyn 6mo ago
Why do you think so? I didn't get such impression.
dang 6mo ago
"Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
jaen 6mo ago
No. Did you even read the article? It talks about the "specification gap", which is the difference between the formalized semantics and the intended semantics. Every formal method has that problem (including the mentioned trivial ones like SAT and SMT).

jaen 6mo ago

There are ways to partially improve or at least quantify the specification gap using LLMs, by analyzing variance in the output formal specification when given a natural language specification (by eg. generating many formal specs from an input description). See eg. "Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning" [1]. [1]: https://arxiv.org/abs/2603.17233 https://arxiv.org/abs/2603.17233