Ask HN: Is the formal methods winter about to end?
Formal methods (theorem proving, model checking, static analysis, abstract interpretation, advanced type systems, program semantics, etc) have remained a relatively niche topic during the last two and a half decades. The field saw much interest during the 1980s and early 1990s. Tony Hoare's 1996 speech recognized formal methods were so far unable to scale to real-world software [1], and that event perhaps marked the beginning of a formal methods winter.
Do you think the field is starting to regain attention? I have observed many positive indicators:
* Strong interest in the mathematics community to mechanize proofs, driven by Lean
* Some technical milestones, such as end-to-end proofs carried by the DeepSpec project
* Emerging synergies with AI, e.g. synthesis
* Some job openings in mainstream companies, e.g. Google
* Respectable number of grant calls and studentships related to the topic, growing from close to zero
* Funded work by cryptocurrency platforms to verify smart contracts, after multi-million fiascos
Is this a promising field to work on? What advances do you expect during this decade?
[1] https://en.wikipedia.org/wiki/Tony_Hoare#Apologies_and_retractions
2 comments
[ 3.1 ms ] story [ 14.5 ms ] threadIf funding, then maybe. You point to some promising signs.
If real world results, then it may thaw... slightly. Formal methods are not going to become very mainstream, though, unless they scale linearly with code base size. Real world code bases are too big for anything else.
The Airbus fly-by-wire code (~100 KLOC) can be statically verified in about an hour with a modern PC.
This is not a formal proof, but it excludes entire classes of runtime errors such as de-referencing a null pointer.