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