Ask HN: Is the formal methods winter about to end?
2 comments
Define "winter". Is it defined by funding, or by real-world results?
If 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.
If 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.
Some things like abstract interpretation scale quite well.
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.
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.
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