[timgebrally]

Perhaps if the methods are sound (even if expensive) then someone can step up and make tooling or refine them so the methods are more accessible to smaller firms. Uncle Bob's opinion's might be discouraging people from exploring them and finding ways to drive down the cost of adopting these better methods.

[Jtsummers]

> Perhaps if the methods are sound (even if expensive) then someone can step up and make tooling or refine them so the methods are more accessible to smaller firms.

To his credit, Hillel is trying to evangelize (in general, not directly through the post linked) a particular tool (TLA+) whose creator (Leslie Lamport) wants to do exactly this. I don't know how big Hillel's employer is, but from what I understand it's nowhere near the biggest engineering firm in number of technical employees. Lamport's current objective with TLA+ is to get people to learn concepts for formal description/specification of systems, and he happens to provide an effective tool for testing those system specs.

Check out his TLA+ tutorial at https://learntla.com.

If you want an example of solving concurrency issues, jump to here: https://learntla.com/concurrency/processes/.

[hwayne]

We have about ten engineers, so nowhere near the size where people consider formal methods "appropriate". Nonetheless it's still been incredibly useful for our work.

I'm a pretty huge evangelist of TLA+, but I don't think it's the silver bullet of software correctness. It just happens to be the tool I'm most familiar with and the one I thought could benefit most from a free guide. If people start widely using TLA+, I'll be ecstatic. If people ignore TLA+ but start widely using Alloy, I'll still be ecstatic. Software correctness is a really huge field and there's lots of really cool stuff in it!

Speaking of making methods more accessible, I'm working on a tutorial about Stateful Testing. Hypothesis (https://hypothesis.works) is an absolutely incredible property-based testing library for Python, and I think it could potentially make PBT a mainstream technique. One of the more niche features is that you can define a test state machine that runs by randomly selecting transitions rules and mutating your program state, then running assertions on the new state. It's really neat!