HN Books @HNBooksMonth

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will.

Besides, TLA+ is not panacea in formal methods. It’s a specification language, which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concepts, such as spurious counterexamples. And remember that essential complexity is in specifying a system? Now try to specify something as simple as quicksort. Let’s just say specifying a system with mathematical logic is beyond 99.99% of software engineers. Not that people are incapable, but I doubt people have enough incentive to swallow the cost. For one, how much does it cost to debug a spec? Don’t believe me, do try out the book by Hehner: http://www.cs.utoronto.ca/~hehner/FMSD/, or introductory books like this: https://www.amazon.com/Verification-Reactive-Systems-Algorit..., and you’ll get the idea. And yes, I thoroughly studied the mentioned books cover to cover and still think they are not for the majority of software engineers.

⬐ zozbot234

The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system. You're making up a simplified "toy" model of your software architecture and verifying claims about your toy model, that may or may not apply to your actual code. This is sometimes justifiable when the software architecture is the most interesting thing you're dealing with, but that's not a very common case. Most programs are designed in relatively simple ways, and would benefit more from an end-to-end system that establishes valuable properties (even comparatively trivial ones like type and memory safety, or simple pre- and post-conditions) about the actual code one will be executing.

⬐ pron

> The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system.

That's a huge benefit, rather than a pitfall at all. End-to-end verification of real-world systems ranges between the impractical through the infeasible to the downright impossible. The biggest software ever verified end-to-end at the same depth as TLA+ was 5x smaller than jQuery, required extraordinary simplification, and still took world experts years. People have found serious bugs in software ten times the size of the largest program even verified end-to-end within days of starting to learn TLA+.

The question is not whether TLA+ can achieve a feat nothing else can, anyway, but whether it has a good ROI.

⬐ hwayne

> It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will.

I've seen people successfully use formal methods on CRUD apps! The trick is to use more lightweight stuff that gets you some benefit without taking as much time. For example, modeling out the problem domain elements and seeing if there's any pathological cases you need to worry about. This is a particularly good use case for Alloy, since it can make visualizations.

⬐ lostcolony

Yep. Anyone who tries to do that in a competitive space will have their lunch eaten by people who slap something together and get it in front of customers.

⬐ pron

> TLA+ is not panacea

Of course it isn't, but neither is testing, and we all still do it. The only question that matters is, does it have a good ROI or not? TLA+ does in a wide range of problems.

> which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concept

That all sounds imposing, but TLA+ users usually don't "master" any of those, and reaching a level of high utility takes far less time than achieving the same with any programming language. Writing useful specifications that can save real money takes something like 3-4 full days of a workshop or 2-4 weeks of after-hours self study. Learning how to read specifications well enough to implement them takes much less (a few hours to one day), and doesn't require any temporal logic at all.

It's certainly possible that it's still not for the majority of engineers, but most teams will have at least one person who can do it, and that might be enough.

> such as spurious counterexamples

???

⬐ tluyben2

> Not that people are incapable

I think that is quite an overestimation of what most people in the industry can do.

⬐ None

None

⬐ SkyMarshal

>but I’m not sure a CRUD app will.

Considering most corporate websites are CRUD apps, and they keep getting pwned via some bug or vulnerability and millions of private user information stolen and pawned off in the black market, I don't think that's an assumption we can make anymore.

That said, full-on formal methods may still be overkill. A web framework built in a language with a strong type system and input sanitation via type-checking and similar safeguards may suffice.

But that's closer to formal methods than most of the web dev industry is accustomed to.

⬐ hwayne

Most of the recent egregious hacks I can think of were compromised by things like out-of-date software, poor access control, stuff on the configuration level. Static analysis might help here, but I don't think formal methods is the lowest-hanging fruit.

⬐ tsimionescu

I'm not sure type safety is the right key here. Rather, better defaults in web and SQL frameworks, even in a dynamic language, would get you most of the way there. You can even use dynamic types to mandate that input is sanitized - a crash is much louder than SQL injection or XSS.

⬐ SkyMarshal

>Rather, better defaults in web and SQL frameworks, even in a dynamic language, would get you most of the way there.

We’ve had 20+ years of building websites, and either we have sane defaults by now but they’re not enough, or we still don’t have sane defaults in our web frameworks.

Either way, that this problem persists given the damage it’s enabling, suggests we haven’t addressed the root cause yet. Web development is still a tarpit, which strong type systems can mitigate in unique ways.

⬐ nicoburns

> You can even use dynamic types to mandate that input is sanitized

If you're using types to mandate that input is santized, then that sounds like type safety to me!

⬐ Akronymus

Good defaults are one of the most important, yet overlooked parts of programming languages IMO.

For example, no nullability or mutability by default is one of the main reasons why I like f#.

https://onor.io/2012/03/27/why-the-defaults-matter/