Ask HN: Is the formal methods winter about to end?

11 points

5 years ago

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