3 ms·
The "why not" list is long and applies to many niche technologies: * No understanding of formal methods. Even someone is working on a problem that TLA+ would b
by zerkten 5y ago
The "why not" list is long and applies to many niche technologies:
* No understanding of formal methods. Even someone is working on a problem that TLA+ would be great at, they don't even know that formal methods exist.
* People aren't given time to apply formal methods. Schedules don't allow for getting things correct. It's hard to persuade management to make space for formal methods for various reasons.
* Other methods of getting the right (or close to it) product and outcome exist. People are more comfortable with building things and testing them rather than using formal methods. They are willing to take a risk with that approach even if there is a strong argument for formal methods.
* People that know/use formal methods tend to gravitate towards niches. Rather than taking on the hard adoption challenges and impacting the culture across large organizations they tend to focus on success niches. Other software engineering mavens are applying arguably easier and less effective processes more successfully across a broad audience.
These don't focus on the product itself. TLA+ has challenges as others point out, but it's hard for it to succeed broadly when there isn't a strong desire for the capability. If the user experience got super slick, then there is a chance that it could become such low effort that people would do it, but this doesn't seem a likely outcome.
- hwayne 5y agoI think there's also a lot we can do to make formal methods easier to learn and use. One of the big things I'm pushing for Alloy is to get a proper CLI so people don't have to do everything through the IDE— this is a surprising source of friction for beginners.
- morelisp 5y agoAs someone who started learning TLA+ in the new year, I'd also add: * The class of bugs it excels at finding which humans can't just aren't that important for most cases! I'm learning it by modeling one of our systems which I know has a race condition that sometimes results in a request being dropped, with the goal of having TLA+ prove it. But if I actually filed this as a bug - three in every ~billion requests get dropped in a process that's already at best reporting 99.9% accurate anyway - it would go straight to the bottom of the backlog. Inconsistent CSS styling of our swagger probably costs us more than this.
- elcritch 5y agoIt’d be more critical in some use cases. Things like DB’s or operating systems would find more value in TLA+. I’m doing embedded work and really want to learn TLA+ at some point.
- nextos 5y agoI think you are spot on. Cryptocurrencies grew very fast to capture the market. They had no time to apply formal methods. But now they are rushing to do so. There are many job offers in the formal methods, a market that was previously close to zero, and they come mostly from blockchain projects. Formal methods have been limited to industries that are very conservative and where code moves slowly. I used them in railway systems and real-time systems for avionics, more than a decade ago. Finding jobs out of that area was not easy. I'm hoping that advances in synthesis, thanks to mixing DL transformers and the already great SAT/SMT solvers, help making formal methods less costly to apply and much more popular. here are lots of interesting and practical ideas in refinement types (e.g. Liquid Haskell), theorem proving (e.g. translators from OCaml to Coq), etc. that would benefit a lot from automation.