4 ms·

Why Don't People Use Formal Methods? – 2019

18 points by chespinoza 5y ago

commandlinefan 5y ago
I love the promise of formal methods. I've been coding professionally since 1992 and to this day, I don't have a better way to get started on a software development task than "give me the gist of what you want, I'll program something, and then we'll tweak it later". Don't get me wrong - I've spent cumulative years of my life sitting through week-long design sessions where the loudest, most opinionated people in the room argue back and forth about trivial, inconsequential details and produce 600+ page documents that no human could possibly read, but none of them have ever had any bearing on the finished product. So I like the idea of having a definite process to go through - however complex - that will result in indisputably superior software. However, even if I were to spend - what, a month? - learning TLA+, I doubt I'm persuasive enough to actually force its adoption in any organization, and there's no real evidence that companies that are actually successful are using it either.
- Tainnor 5y ago
  Apparently, Amazon is using TLA+ to some extent or another.
  - DylanSp 5y ago
    Yep, at least on the AWS side. See https://m-cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext https://m-cacm.acm.org/magazines/2015/4/184701-how-amazon-we...
  - tluyben2 5y ago
    TLA+ is a good way to get into to some formalization: it is easy to learn.
- DylanSp 5y ago
  Check out https://www.hillelwayne.com/post/business-case-formal-methods/ https://www.hillelwayne.com/post/business-case-formal-method... (from the same author as the OP). It's a blogpost on how to make the case for adopting formal methods, including links to case studies about its use in industry.
errantmind 5y ago
Perhaps a lack of compelling success stories? There are lots of approaches that work well on paper but fall apart out in the wild.
rurban 5y ago
All my latest projects do have a `make verify` target. It's not much work, and it tests much more than 100% code coverage. I'm always surprised what kind of weird bugs it finds. Eg in my CTL (the STL in C) it found the 3way comparison problem, which was just recently added to the STL.

18 points by chespinoza 5y ago

I love the promise of formal methods. I've been coding professionally since 1992 and to this day, I don't have a better way to get started on a software development task than "give me the gist of what you want, I'll program something, and then we'll tweak it later". Don't get me wrong - I've spent cumulative years of my life sitting through week-long design sessions where the loudest, most opinionated people in the room argue back and forth about trivial, inconsequential details and produce 600+ page documents that no human could possibly read, but none of them have ever had any bearing on the finished product. So I like the idea of having a definite process to go through - however complex - that will result in indisputably superior software. However, even if I were to spend - what, a month? - learning TLA+, I doubt I'm persuasive enough to actually force its adoption in any organization, and there's no real evidence that companies that are actually successful are using it either.

Tainnor 5y ago
Apparently, Amazon is using TLA+ to some extent or another.
- DylanSp 5y ago
  Yep, at least on the AWS side. See https://m-cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext https://m-cacm.acm.org/magazines/2015/4/184701-how-amazon-we...
- tluyben2 5y ago
  TLA+ is a good way to get into to some formalization: it is easy to learn.
DylanSp 5y ago
Check out https://www.hillelwayne.com/post/business-case-formal-methods/ https://www.hillelwayne.com/post/business-case-formal-method... (from the same author as the OP). It's a blogpost on how to make the case for adopting formal methods, including links to case studies about its use in industry.

errantmind 5y ago

Perhaps a lack of compelling success stories? There are lots of approaches that work well on paper but fall apart out in the wild.

rurban 5y ago

All my latest projects do have a `make verify` target. It's not much work, and it tests much more than 100% code coverage. I'm always surprised what kind of weird bugs it finds. Eg in my CTL (the STL in C) it found the 3way comparison problem, which was just recently added to the STL.