3 ms·
I still see your point but quoting the How Amazon Web Services Uses Formal Methods paper: In each, TLA+ has added significant value, either finding subtle
by CalChris 7y ago
I still see your point but quoting the How Amazon Web Services Uses Formal Methods paper:
In each, TLA+ has added significant value,
either finding subtle bugs we are sure
we would not have found by other means,
or giving us enough understanding and
confidence to make aggressive performance
optimizations without sacrificing correctness.
Type checking, borrow checking and unit testing are similar albeit weaker tools that allow rapid development by providing a safety net.
- tptacek 7y agoI'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.
- pron 7y agoThe 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.