Read on Twitter
Let& #39;s dig into "Formal Methods branding".
Hypothesis: "Formal Methods" is largely avoided in branding for the most-used projects that have come out of the Formal Methods field.
"Most used" in this thread means commercial use spread beyond the originating company.
1/
Hypothesis: "Formal Methods" is largely avoided in branding for the most-used projects that have come out of the Formal Methods field.
"Most used" in this thread means commercial use spread beyond the originating company.
1/
To @fbinfer first. The infer homepage mainly describes the tool as a "static analysis". This is great! It emphasizes that the tool is fast and light. Developers likely get good feelings when they think of static analyses.
https://fbinfer.com/
2/">https://fbinfer.com/">...
https://fbinfer.com/
2/">https://fbinfer.com/">...
Infer is very much a "Formal Methods" tool, however. It& #39;s a descendant of academic tools built around separation logic.
The beginning of that story is here:
https://research.fb.com/wp-content/uploads/2016/11/publication00124_download0001.pdf
That">https://research.fb.com/wp-conten... paper uses the phrase "Formal verification", but not "formal Methods"
3/
The beginning of that story is here:
https://research.fb.com/wp-content/uploads/2016/11/publication00124_download0001.pdf
That">https://research.fb.com/wp-conten... paper uses the phrase "Formal verification", but not "formal Methods"
3/
It seems like use of Infer has spread quite well, they list a number of companies that use it
4/
4/
The branding for ErrorProne is similar, and the outcomes are related as well. I don& #39;t know the origin story well enough to know if Formal Methods gets to claim that one as a success story though, although we& #39;d be lucky to...
https://errorprone.info/index
5/">https://errorprone.info/index&quo...
https://errorprone.info/index
5/">https://errorprone.info/index&quo...
TLA+ seems very successful in spreading to a wide range of use. Its website describes it as a modeling tool. No mention of Formal Methods at all, although it& #39;s unquestionably a FM tool through and through.
https://lamport.azurewebsites.net/tla/tla.html
6/">https://lamport.azurewebsites.net/tla/tla.h...
https://lamport.azurewebsites.net/tla/tla.html
6/">https://lamport.azurewebsites.net/tla/tla.h...
F* has had loads of impact, although I& #39;m not sure how far its use has spread beyond Microsoft Research and academia. The tagline is:
"F* is a general-purpose functional programming language with effects aimed at program verification"
https://www.fstar-lang.org/
7/">https://www.fstar-lang.org/">...
"F* is a general-purpose functional programming language with effects aimed at program verification"
https://www.fstar-lang.org/
7/">https://www.fstar-lang.org/">...
F* gets big points for ease of installation and a install-free tutorial.
It doesn& #39;t describe itself as formal methods, but the tagline will definitely be a friendlier read to someone in the FM space than outside.
8/
It doesn& #39;t describe itself as formal methods, but the tagline will definitely be a friendlier read to someone in the FM space than outside.
8/
SPARK Ada is the first tool in this thread that depends on external sales for continued existence, and it shows.
The description is a "Software development technology" which is an accessible way to describe what it does
https://www.adacore.com/about-spark
9/">https://www.adacore.com/about-spa...
The description is a "Software development technology" which is an accessible way to describe what it does
https://www.adacore.com/about-spark
9/">https://www.adacore.com/about-spa...
To a FM person that knows what& #39;s actually in there, that might feel like an underwhelming description, but perhaps it pays to be a bit underwhelming up front to catch people& #39;s attention without scaring them away.
10/
10/
It& #39;s hard to say if AFL is really a Formal Methods tool. Honestly, if you& #39;re as broadly useful to as many projects as AFL is, you probably don& #39;t need to worry that much about how you sell yourself.
https://lcamtuf.coredump.cx/afl/
11/">https://lcamtuf.coredump.cx/afl/"...
https://lcamtuf.coredump.cx/afl/
11/">https://lcamtuf.coredump.cx/afl/"...
The same goes for Valgrind. If you build a tool that can turn up aggravating bugs, almost for free. I think people will use it
https://valgrind.org/
12/">https://valgrind.org/">...
https://valgrind.org/
12/">https://valgrind.org/">...
AbsInt is a company that uses a range of tools, all unarguably formal methods. They describe their work as
"Unique tools and services for the development,
analysis, and certification of safety-critical software."
https://www.absint.com/
13/">https://www.absint.com/">...
"Unique tools and services for the development,
analysis, and certification of safety-critical software."
https://www.absint.com/
13/">https://www.absint.com/">...
The description gives a similar feeling to SPARK, which I still think is good. That it casually hides game-changing tools like Astrée and Compcert behind that description is amusing.
I have no idea how often the tool application is done by absint vs their customers
14/
I have no idea how often the tool application is done by absint vs their customers
14/
But they& #39;ve got loads of big customers regardless, with Airbus as the most noteworthy:
https://www.absint.com/success.htm
15/">https://www.absint.com/success.h...
https://www.absint.com/success.htm
15/">https://www.absint.com/success.h...
Stopping now, this already took longer than I expected. I meant to do more, and I& #39;d love to talk more about any company or tool on or off of this list.,
16/
16/
Conclusion: Nobody even mentioned Formal Methods, but FM might still be a valuable concept. If I am a software engineer or manager and I want to know how FM might help me, where do I go?
Depending on the application the answer could be a huge range of things.
17/
Depending on the application the answer could be a huge range of things.
17/