Re:Formal Verification Creates Hacker-Proof Code (2016)
by tptacek on Sunday April 26, 2020 @03:23PM
(#22989454)
I'm on the "yes type checking" side of the perennial "which is more efficient" programming language debate, but when we talk about "formal methods" in the context of eradicating security vulnerabilities, the subtext is "formally proving correctness", not simply any tool that increases rigor. I agree, boringly, that there are PL tools that apply rigor to increase development speed.
[ Parent
| on HN ]
Re:Formal Verification Creates Hacker-Proof Code (2016)
by pron on Friday May 01, 2020 @07:34PM
(#23047602)
The belief that software could be affordably proven correct was pervasive in the 70s, it led to a research winter, and now formal methods is very much about adding rigor and catching more bugs (some of the most promising directions in contemporary formal methods research revolve around reducing soundness to help find more bugs more quickly).
There is a small subdiscipline of formal methods that comes from programming language theory (judging by conferences, it makes up no more than 10-20%) that does still have this 1970s "subtext", but actual researchers or practitioners are usually careful with what they actually say, and you'll most often find such claims explicitly made only by fans.