Read on Twitter
Let'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/
2/
Infer is very much a "Formal Methods" tool, however. It'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 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 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't know the origin story well enough to know if Formal Methods gets to claim that one as a success story though, although we'd be lucky to...
https://errorprone.info/index
5/
https://errorprone.info/index
5/
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's unquestionably a FM tool through and through.
https://lamport.azurewebsites.net/tla/tla.html
6/
https://lamport.azurewebsites.net/tla/tla.html
6/
F* has had loads of impact, although I'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/
"F* is a general-purpose functional programming language with effects aimed at program verification"
https://www.fstar-lang.org/
7/
F* gets big points for ease of installation and a install-free tutorial.
It doesn'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'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/
The description is a "Software development technology" which is an accessible way to describe what it does
https://www.adacore.com/about-spark
9/
To a FM person that knows what'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's attention without scaring them away.
10/
10/
It's hard to say if AFL is really a Formal Methods tool. Honestly, if you're as broadly useful to as many projects as AFL is, you probably don't need to worry that much about how you sell yourself.
https://lcamtuf.coredump.cx/afl/
11/
https://lcamtuf.coredump.cx/afl/
11/
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/
12/
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/
"Unique tools and services for the development,
analysis, and certification of safety-critical software."
https://www.absint.com/
13/
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'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.htm
15/
Stopping now, this already took longer than I expected. I meant to do more, and I'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/
I'll finish with the questions I have.
Is grouping tools and approaches as "formal methods" actually useful?
Is it worth thinking about how to advertise these tools to non FM people?
If I'm a possible early user of Formal Methods, what should I be doing?
18/18
Is grouping tools and approaches as "formal methods" actually useful?
Is it worth thinking about how to advertise these tools to non FM people?
If I'm a possible early user of Formal Methods, what should I be doing?
18/18
