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. [\n] Do you think the field is starting to regain attention?
People asked for my thoughts, and they went a bit long as a response, so I'm making it a newsletter. Caveat, since this is a newsletter and not a full post I'm not doing as much research as I normally would: this is all off the top of my head.1 Also, I'm going to be treating formal methods as a giant homogeneous mass, in particular blurring the code/model distinction between approaches. A more serious essay would talk about them separately. I'm assuming you don't have a background in FM but have the info of an "educated outsider", about as much as this essay covers.
First of all, one assumption in the question I need to address: there has not been a formal methods winter. The term comes from the AI Winter(s), where the industry suddenly and dramatically lost interest in AI. The same thing never happened to FM, because there never was any industry interest in the first place.