Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why Don't People Use Formal Methods?

hillelwayne.com

Post reply on HN
Print view View original

51–60 of 232 posts

Re: Why Don't People Use Formal Methods?

#51

Post by adrianratnapala »

Jtsummers wrote: post #29
twblalock wrote: post #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 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 wi…

> That behavior won't change from week-to-week

Maybe "shouldn't" is a better world that "won't".

It is sadly common for a sudden whim to cause a new feature to thread a change all the way from the GUI down to the database representation, with plumbing at multiple stages in the middle.

Re: Why Don't People Use Formal Methods?

#52

Post by xiphias2 »

xvilka wrote: post #49
xiphias2 wrote: post #41

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well:…

This is why currencies like Cardano were created.

Cardano's proof of stake model has stronger assumptions than proof-of-work (if it wouldn't be the case, and the authors could prove it, they could work on improving Bitcoin itself...but I think they preferred to make money).

New altcoins just don't solve the problem of increasing the security of Bitcoin. Schnorr signatures are are great example of not making the cryptographic assumptions stronger (actually making them weaker) while improving the scalability of the system.

Re: Why Don't People Use Formal Methods?

#53

Post by mikekchar »

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and inclination to investigate the details are not the ones who care what it does. You can have an incredibly low defect count and still not build the thing you need.

But if you look at a lower level of specification, then formal methods start making a lot more sense. For example, let's say I have to implement a communications protocol. This is something I can specify and that I can build against that specification. Companies sell protocol testers that test your implementation against a protocol. It might be nicer to have a formal specification than a back end test -- especially because there are often more scenarios you care about than you can feasibly test.

At an even smaller scale, we are now realising some benefits of this mode of thinking. For example, we've had types in programming languages for a long time, but lately we're able to actually make statements about what the code does, simply by analysing the types. This is a massive step forward and I'm really looking forward to things like constrained types making it into the mainstream. Similarly things like Rust's borrow checker can allow you to make analytical statements about how much memory you are using (if you are careful), etc, etc. These are great.

I think that the success of formal methods is going to be through the backdoor and at this design/implementation level for a long time. In fact, pretty much forever.

Re: Why Don't People Use Formal Methods?

#54

Post by mshockwave »

Jtsummers wrote: post #29
twblalock wrote: post #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 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 wi…

totally agree, formal specs usually used to describe the desired _goals_ of the project, so it's pretty high level and probably won't change pretty often

Re: Why Don't People Use Formal Methods?

#55

Post by chubot »

cjensen wrote: post #34

Do people read "The Mythical Man-Month" anymore? The answer to questions like these are part of the book. First, there is no "Silver Bullet" which makes software development easy. Second, adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount. I'm not suggesting that you avoid Formal Methods. It might really fit…

I think you're making a good point, but your tone is unnecessarily strident.

Re: Why Don't People Use Formal Methods?

#56

Post by Palomides »

maxyme wrote: post #38

I did an internship at a company building aviation hardware and software. Since everything was safety critical we used formal methods and things moved at a snail's pace. When verification becomes the most important thing everything changes. The design specification doesn't make sense? It will take months to get it changed, write whatever code you can convince someone verifies against the design. Compile times are lon…

are you able to share which company? I'm just curious since during my aviation software experience I only heard we were just looking into maybe adding some formal methods approaches.

Re: Why Don't People Use Formal Methods?

#57

Post by throwawayjava »

cjensen wrote: post #34

Do people read "The Mythical Man-Month" anymore? The answer to questions like these are part of the book. First, there is no "Silver Bullet" which makes software development easy. Second, adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount. I'm not suggesting that you avoid Formal Methods. It might really fit…

> there is no "Silver Bullet"

Your second paragraph kind of walks back on this, but I think it's still worth linking to this essay:

https://www.hillelwayne.com/post/uncle-bob/

In particular: ...[he's] welcome to keep shouting that tools won’t help, better languages won’t help, better process won’t help, the only thing that’ll help is lots and lots of unit tests. Meanwhile, we’ll continue to struggle with our bugs, curse our model checkers, and make software engineering just a little bit better. We don’t believe in silver bullets.

Again, your second paragraph already kind of agrees with this point, but the brilliant rhetoric in the essay is actually true: "no silver bullets" is a reason for, not against, the use of formal methods (and any other quality assurance mechanism we can get!)

> adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount.

It really depends. Especially in the case of formal methods for specification (as opposed to implementation formal methods), formal methods can save substantial amounts of time and manpower. And there are already a lot of success stories, and not just in safety-critical industries.

Re: Why Don't People Use Formal Methods?

#58

Post by tdonovic »

westurner wrote: post #42

Which universities teach formal methods? - q=formal+verification https://www.class-central.com/search?q=formal+verification - q=formal-methods https://www.class-central.com/search?q=formal+methods Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs? Is there a certification for formal methods? Something like for engi…

Almost University of New South Wales (Sydney, Australia) alum, and it's the biggest difference between the Software Engineering course and Comp Sci. There are two mandatory formal methods and more additional ones to take. They are really hard, and mean a lot of the SENG cohort ends up graduating as COMPSCI, since they can't hack it and don't want to repeat formal methods.

Re: Why Don't People Use Formal Methods?

#59

Post by Jtsummers »

chubot wrote: post #55
cjensen wrote: post #34

Do people read "The Mythical Man-Month" anymore? The answer to questions like these are part of the book. First, there is no "Silver Bullet" which makes software development easy. Second, adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount. I'm not suggesting that you avoid Formal Methods. It might really fit…

I think you're making a good point, but your tone is unnecessarily strident.

I'll disagree, I don't think they're making a good point.

GP implies that formal methods always add time to projects, which is going to be true for:

1) Projects that are building the wrong thing and spend time verifying the wrong thing (failed validation)

2) Projects with people inexperienced in formal methods (most projects today)

The latter is just a matter of experience. Once people get used to thinking about things in a more formal way, they'll get faster. Additionally, they'll learn which parts need to be shown formally and which don't (or which parts they can show via their type system versus those which need to be modeled outside the language and type system, etc.). I don't need to formally prove that my program writes message X to memory block Y, it can be verified by: inspection, tests. I do want to prove that my two processes correctly exchange messages (since the nature of the system is such that we needed to write our own protocol rather than being able to rely on a pre-built and verified/validated one). But here I'm proving the protocol, I still have to test the implementation (unless my language permits me to encode proofs in a straightforward way).

The former is a separate issue from formal methods. It's failed validation efforts which is solved (or mitigated) by something else: lean/agile approaches to project management (versus delaying feedback from customers, and consequently delaying validation activities).

Re: Why Don't People Use Formal Methods?

#60

Post by mullr »

hwayne wrote: post #23
ejcx wrote: 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…

Can’t speak for aerospace, but at least for automotive systems, the functional safety standards that dictate what you have to do for the most critical parts of the system are kind of a joke. They amount to a lot of test coverage, lint tooling, and extensive requirements management that manages to still be full of gaping holes. Formal methods are suggested on a “wouldn’t it be nice” level, but nobody thinks they can afford it. There are a lot of reasons for this; inertia, inexperience with formal methods, and the difficulty of the tools comes to mind. None of them are acceptable excuses, especially as we are asked to turn more and more control over to increasingly sophisticated ADAS (eventually autonomy) systems.
Post reply on HN