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, 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?