← Back to context

Comment by GZGavinZhao

2 days ago

Formal Methods in general are underrated in the industry. Pretty much no large companies except AWS (thank you Byron Cook!) use them at a large scale.

Edit: maybe there are large companies that use them behind the curtains, but AWS is the only place I know of where they publicly acknowledge how much they appreciate and use formal methods. If you know any of them, please comment and I'd be curious to learn about how they're using it!

8 comments

GZGavinZhao

Reply
Twirrim  2 days ago

Microsoft, Amazon, Oracle, Google, all sorts of large companies use them, and talk about it, publicly. They've all published whitepapers and resources about them. Microsoft even employs Dr. Leslie Lamport who created and maintains TLA+ (among other things).

Just for some quick examples:

Microsoft: https://github.com/Azure/azure-cosmos-tla, https://www.youtube.com/watch?v=kYX6UrY_ooA

Google: https://research.google/pubs/specifying-bgp-using-tla/, https://www.researchgate.net/publication/267120559_Formal_Mo...

Oracle: https://blogs.oracle.com/cloud-infrastructure/post/sleeping-... (note the author is a "Formal Verification Engineer", it's literally his job at Oracle to do this stuff)

Intel: https://dl.acm.org/doi/10.1145/1391469.1391675, https://link.springer.com/chapter/10.1007/978-3-540-69850-0_...

Jetbrains: https://lp.jetbrains.com/research/hott-and-dependent-types/

Arm: https://ieeexplore.ieee.org/document/9974354

  • dfc  2 days ago

    Lamport+Microsoft was the first thing that I thought of when I read the comment. FWIW he retired at the beginning of this year.

IshKebab  2 days ago

I don't think they are underrated. They are heavily used where they work really well and bugs have a very high cost (e.g. hardware design).

For the vast majority of software though they don't really make much sense because formally verifying the software is 10-100x more work than writing it and testing it with normal methods. And formal verification of software generally requires faaaaar more expertise than most people have. (The situation is much better for hardware design because it tends to be way simpler.)

It's a very powerful tool but also extremely difficult to use.

steamrolled  2 days ago

> Formal Methods in general are underrated in the industry. Pretty much no large companies except AWS (thank you Byron Cook!) use them at a large scale.

At least Microsoft and Google poured a lot of money into this by funding well-staffed multi-year research projects. There's plenty of public trail in terms of research papers. It's just that not a whole lot came out of it otherwise.

The problem isn't that the methods are underrated, it's that they aren't compatible with the approach to software engineering in these places (huge monolithic codebases, a variety of evolving languages and frameworks, no rigid constraints on design principles).

  • fakedang  1 day ago

    Can you ELI5 what formal methods are and how not the industry standard apparently? As a complete noob, from what I'm reading online, they're pretty much how you should approach software engineering, or really any sort of programming right?

    • dwrodri  1 day ago

      Formal methods = “this software cannot do things it shouldn’t do”, I have formally proven it ALWAYS EXECUTES THE WAY I CONSTRAINED IT TO.

      Contrast with

      Testing = “My tests prove these inputs definitely produce these test outputs”

      IME Formal methods struggle making contact with reality because you really only get their promise “it always does what it is constrained to do” when every abstraction underneath provides the same guarantee, I wager most CPUs/GPUs aren’t verified down to the gate level these days.

      It’s just faster to “trust” tests with most of the benefit, and developing software faster is very important to capturing a market and accruing revenue if you are building your software for business reasons.

      EDIT: My gate-level verification remark is a bit extreme, but it applies to higher layers of the stack. The linux kernel isn’t verified. Drivers are sometimes verified, but not often. There is an HN comment somewhere about building a filesystem in Coq, and while the operations at the filesystem layer are provably correct, the kernel interfaces still fail. The firmware still isn’t proven. The CPU itself running on has undisclosed optimizations in its caches and load/store mechanisms which just aren’t proven, but enabled it to beat the competition on benchmarks, driving sales.

      1 reply →