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

31–40 of 232 posts

Re: Why Don't People Use Formal Methods?

#31

Post by Tempacc78534 »

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…

Not True.

Agile Dev (according to me) means you are trying to specify what the customer want as you develop your code and not specify it right in the beginning.

You can make changes to the specs when you are figuring things out. Also, you do verification when you are somewhat confident in your code is doing what the customer wants, so verification should come towards the end of your development phase (or at least end of developing parts of your code base).

Re: Why Don't People Use Formal Methods?

#32

Post by ejcx »

Jtsummers wrote: post #27
hwayne wrote: post #23

Earlier quoted context omitted.

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 te…

Jtsummers, I don't disagree with you. The reality is the DO-178C is no different than PCI or other compliance standards, and there are ways to game it with docs.

With that said, if formal methods were really required to fly the plane then they would add it to the DO-178[D] without hesitation =]

Re: Why Don't People Use Formal Methods?

#33

Post by zzzcpan »

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…

I don't think it's about agile, even with waterfall "you still don't know what you are actually making" as another comment put it.

Making software is how you figure out what you are making. Formal methods are just philosophically incompatible with that. Software is how you learn the world and formal methods is how you create it, you can't have both and we don't really have much use for creating worlds.

Re: Why Don't People Use Formal Methods?

#34

Post by cjensen »

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 your needs -- for example, if you need high-quality code and can afford the expense, Formal Methods may fit the bill. The important thing is that not all development projects have the same needs.

Re: Why Don't People Use Formal Methods?

#35

Post by hwayne »

timClicks wrote: post #2

Absolutely love that Hillel seems to have single-handedly assumed the role of taking formal methods to the people. His Apress title ( https://www.apress.com/gp/book/9781484238288 ) is a wonderful example of technical writing that's somehow accessible, yet deep.

You might also like _Software Abstractions_ (https://mitpress.mit.edu/books/software-abstractions-revised...), by Daniel Jackson. I read the whole thing in two days and then immediately emailed him gushing about how much I loved the book. It's absolutely fantastic.

Re: Why Don't People Use Formal Methods?

#36

Post by Tempacc78534 »

hwayne wrote: post #25
Tempacc78534 wrote: post #7

Earlier quoted context omitted.

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.

It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies.

Also, a little nitpicking in your write up but you should have also talked about type systems. They carry the spirit of formal methods but rather than being construct then check for correctness, are construction is correct by default. Type systems are widely accepted and show that some of these ideas can gain traction.

Re: Why Don't People Use Formal Methods?

#37

Post by ggm »

because (as the fine article says) "proofs are hard"

we don't do hard. we don't use APL. we don't use z or coq or isabel or any number of things, because we don't like hard things.

proofs are hard. its that simple.

Re: Why Don't People Use Formal Methods?

#38

Post by maxyme »

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 longer than an hour? Not a problem since the majority of the job isn't writing code but instead doing code reviews, verifications and writing tests. In fact writing code was about 15% of that job for the lowest level engineer. It was a whole different world than unregulated codebases are.

Re: Why Don't People Use Formal Methods?

#39

Post by hwayne »

earthicus wrote: post #15

Does anyone here have any experience using semi-formal methods, like 'cleanroom' techniques? The commentaries I've heard (e.g. [1]) tend to be very enthusiastic, but I don't have enough experience to judge their credibility so I'd love to hear what others have to say on the matter. [1] http://infohost.nmt.edu/%7Eal/cseet-paper.html

At one point a while back I emailed Stavely to learn more about how it's changed over time, but he's been out of the software world for over a decade now. Of the people I've met who've been on cleanroom projects, the _tentative_ impression I got is that it's fast and it works but it's really taxing on the people involved. One of these days I want to do more careful interviews and the like.

Re: Why Don't People Use Formal Methods?

#40

Post by tnecniv »

hwayne wrote: post #25
Tempacc78534 wrote: post #7

Earlier quoted context omitted.

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.

I don't know how it's used in practice, but aviation companies dump a lot of money into formal methods research because getting their code certified to meet scary specs is very expensive and they don't want to do it for every bug fix.
Post reply on HN