Live data from Hacker News

Why Don't People Use Formal Methods?

hillelwayne.com

21–30 of 232 posts

Re: Why Don't People Use Formal Methods?

#21
post #8
post #5

I think it goes beyond conservatism for most devs as to why you don't formally specify your design and its mostly rooted in why AGILE is so popular. The sooner you show a finished product, no matter how broken and incomplete, the sooner your client can realize all the things they didn't want they said they did and replace them. If you give them a formal design document it might be ironclad and foolproof but it doesn'…

Unlike the case of building an airplane, when you’re developing software you don’t know when you start sometimes if you want to build an airplane or a helicopter, or even if you want to fly, or indeed, if you’re building a vehicle of any kind, and not some kind of corn mill or a movie theater, perhaps.

The thing about software, indeed, most of it isn't space shuttles or life support systems. But it can go from paper airplanes to model airplanes to real airplanes more quickly than you'd think. Your hobby website could take-off to be an income and then a company and have leftover code all around.

Re: Why Don't People Use Formal Methods?

#22
The question begged on formal methods is, who is the customer of the design? To accept a formal design, you must also be bound by the constraints and timelines it specifies, which reduces your flexibility.

The perception the OP or someone here might correct is, formal methods frustrate corner cutting and other product level optimizations that return margins, optionality, performance bonuses, positioning and leverage, "moving the needle," and other higher order fudges that are realities of human organization.

One example is how producing a security design to provide assurances to exogenous stakeholders becomes a forcing function on feature commitments. e.g. "if you do this feature, you need these controls, which means if you don't have those controls, you aren't delivering the feature by date X, and now there is a paper trail that you know that. have fun at the customer meeting!" This is a crude example, but makes the point.

From a product and exec perspective, that forcing function knocks the ball out of the air / collapses the wave function in regard to "who knew what when," as it relates to making feature commitments to customers, sales people, and channel partners, etc. These are all people whose interests are not necessarily aligned. Much of enterprise tech business is keeping that equilibrium unstable in a kind of strategic fog while you build a coalition of stakeholders that gets your company paid. A methodology that forces decisions in those relationships will get mutinied by sales pretty fast.

(It's often hard to tell whether people are solving these higher order alignment problems or just being dishonest, and many of them don't even know for themselves.)

In this sense, formal methods solve engineers problems but not necessarily business problems. Playing the cynical customer, I don't care how much marginal residual risk there is, I only care who holds it. Above a certain level, detail just means "caveat emptor."

It's a critical view of org behavior, but finding a customer for the models themselves (other than compliance) would go a long way to getting them adopted.

Re: Why Don't People Use Formal Methods?

#23
post #19

Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B. Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.

I had a section on "high-availability software" that I cut due to not being able to research it thoroughly. For the most part cars and medical devices and stuff don't use FM because there's pretty much no oversight. Aircraft, though, are a super interesting case here. I'll be honest, I'd probably trust code that's gone through DO-178C more than I would trust code that's been formally verified.

I _believe_ there's been a push to add formal methods to avionics, mostly because it'd potentially save money. But any FM stuff has to go through DO-330 and DO-333, which are just as rigorous and intense as DO-178C. The only stuff that has so far is, unsurprisingly, very expensive and very proprietary.

Re: Why Don't People Use Formal Methods?

#24

> Why Don't People Use Formal Methods? Because they're an emerging and unproven technology? Why don't people rewrite everything in Rust? That would surely be a lot more straightforward than adopting the sorts of "formal methods" where you only write a handful of (C-language equivalent) LOC per day, across the software industry! So why doesn't it happen? There's your answer.

Formal Methods are 30+ years old.

https://en.wikipedia.org/wiki/Formal_methods

Re: Why Don't People Use Formal Methods?

#25
post #5

I think it goes beyond conservatism for most devs as to why you don't formally specify your design and its mostly rooted in why AGILE is so popular. The sooner you show a finished product, no matter how broken and incomplete, the sooner your client can realize all the things they didn't want they said they did and replace them. If you give them a formal design document it might be ironclad and foolproof but it doesn'…

You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code. Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somew…

I didn't include it in the article because I wasn't 100% confident in saying so, but I'm reasonably sure that medical devices don't use FM. There's not a whole lot of oversight in that area, and most of the standards are (to my knowledge) about software process versus software methods.

Aviation also doesn't really use FM, but that's because they follow DO-178C, and that is a scary scary standard.

Re: Why Don't People Use Formal Methods?

#26
Formal methods don't make a lot of sense when the product changes from week to week, or month to month, or even year to year.

It seems like the advocates of formal methods assume a waterfall method of software development wherein you develop a spec, formalize it, prove that it works, and then deliver it. That's just not how software works in industry. A lot of it never had formal specs and never will, and whatever specs exist change frequently. By the time a spec is perfected it is out of date and we are already moving on to the next thing.

Agile development killed waterfall development and formal methods have not adapted to the agile methodology.

Re: Why Don't People Use Formal Methods?

#27
post #23
post #19

Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B. Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.

I had a section on "high-availability software" that I cut due to not being able to research it thoroughly. For the most part cars and medical devices and stuff don't use FM because there's pretty much no oversight. Aircraft, though, are a super interesting case here. I'll be honest, I'd probably trust code that's gone through DO-178C more than I would trust code that's been formally verified. I _believe_ there's bee…

Having worked on aircraft software, including some very safety critical stuff, I wouldn't necessarily trust code that went through DO-178(A|B|C).

There's an unfortunate tendency (just like CMMI and other certifications needed/desired in that industry) to achieve the certification on paper by backfilling. DO-178 requires a formal spec document (NB: Not the same as formal methods) with traceability to the design and test procedures. Oops, we let it get stale (Read: Didn't keep up to date). I've seen people turn that into 5k pages with a good enough looking RTM that no one was ever going to read, and it got certified.

A system I recently worked on (left the project, it was toxic, or maybe it was me) had a "design" document that consisted of running the code through doxygen. While that did produce documentation, the code was reasonably completely annotated, it did not produce a design document (which should include rationales and things like, I don't know, state transition diagrams or similar to illustrate the design, not just the structure). And that system is flying today (has been for a while).

These things turn into games by the developers and managers, like hitting 100% code coverage in testing (which doesn't mean you've actually verified/validated anything).

Re: Why Don't People Use Formal Methods?

#28
post #24

> Why Don't People Use Formal Methods? Because they're an emerging and unproven technology? Why don't people rewrite everything in Rust? That would surely be a lot more straightforward than adopting the sorts of "formal methods" where you only write a handful of (C-language equivalent) LOC per day, across the software industry! So why doesn't it happen? There's your answer.

Formal Methods are 30+ years old. https://en.wikipedia.org/wiki/Formal_methods

AI is 30+ years old too, and formal methods (especially things like solving SAT, or theorem proving) used to be considered AI. I'm not quite sure what your point is; just because something has a 30+ years history doesn't somehow make it a mature, usable tech.

Re: Why Don't People Use Formal Methods?

#29

Formal methods don't make a lot of sense when the product changes from week to week, or month to month, or even year to year. It seems like the advocates of formal methods assume a waterfall method of software development wherein you develop a spec, formalize it, prove that it works, and then deliver it. That's just not how software works in industry. A lot of it never had formal specs and never will, and whatever sp…

Formal methods make sense when you focus them on the right part of your system. Even if it's changing week-to-week, there's an underlying structure or design that's staying consistent.

You wouldn't use formal methods on, say, the GUI layout of your system. But you could use it to prove that you're accessing your database in a way that won't cause corrupted or incorrect data to appear. If you're working on anything with concurrency, this is actually crucial. Show, for instance, that your multi-user Google Docs clone won't end up with a corrupted document when two users try to edit the same sentence or word at the same time.

That behavior won't change from week-to-week (both the multi-user nature and the desire for stability/reliability), though the nature of the interface or target platforms may change.

Also, Waterfall only existed because some people at NASA/DOD were idiots and couldn't read past the intro to Royce's paper. It needs to die a terrible death.

Formal methods can happily exist within an agile environment once you realize that you don't have to deliver code each week. You are able to deliver prototypes, mockups, and documents along the way. Formal models can exist in that group.

Re: Why Don't People Use Formal Methods?

#30

> Why Don't People Use Formal Methods? Because they're an emerging and unproven technology? Why don't people rewrite everything in Rust? That would surely be a lot more straightforward than adopting the sorts of "formal methods" where you only write a handful of (C-language equivalent) LOC per day, across the software industry! So why doesn't it happen? There's your answer.

Static type checking is abstract interpretation. If you program in Java you are using formal methods.
Post reply on HN