← Back to context

Comment by 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).

3 comments

steamrolled

Reply
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.