Ask HN: Why don't you use formal methods?

Maybe this is just my ignorance speaking, but I think that using formal methods would take a lot of time; more than the projects I am working on are worth.

Also, I don't know how to do it. I mean, at school we had some examples, but those were for math-like stuff (how to verify that the algorithm calculating the square root actually calculates the square root), but I wouldn't know how to apply that to programs that are mostly reading something from database and displaying it on a web page.

Now that I googled a bit, I found a paper https://arxiv.org/abs/1809.03162 claiming that "Tools for formal verification of Java programs are in generally poor shape, and do not support recent versions of Java". That would explain why smarter people around me are also not using them.

Give me a tool that is easy to install and works reliably, and I will be happy to learn a new thing.

I think the book Zen and the Art of Motorcycle put it well. Formal methods are unstoppable but they're also really slow.

A lot of it is incorrect too. For example, there are methodologies to doing software estimation. Some of the more complex ones are less accurate than some of the simpler ones. Nobody really cares that there's a 90% chance that this feature will be completed between 4 hours and 4 months, and a 30% chance that it will be completed in 2 weeks. If asked for an estimation, someone will just toss out the "2 weeks number" because it has the highest odds. Nor do you really want to spend several hours or days narrowing that range, because not only would you still be incorrect, you'll have spent time on estimation that you otherwise would have spent doing work.

1. Yes, I did a deep dive into TLA+ (Hillel's publications are great for this) and used it as a proof of concept (attempted to convince the office to use it) to demonstrate the nature of a bug (I described how we thought the system behaved (per spec), no issues, then recreated the bug by selectively weakening the model, which mirrored exactly the problems in the real system). I've also used TLA+ as a model checker for non-programming systems to demonstrate where we could anticipate errors/problems and strengthen policy, physical, or software controls to prevent/mitigate them, that was a side project for me but the information was used by my sister professionally. That worked well because real world systems are inherently concurrent. It was another case of trying to convince management that simulation/modeling was good (it worked in her case, to some extent).

2. Some of it, not all of it. (1) was a concurrency issue and was well-suited to TLA+'s approach. Present office does not deal with concurrency to the same extent so I wouldn't try to sell TLA+ here. Other methods would be more appropriate (especially things like proper state diagrams/statecharts which are amenable to simulation, versus the traditional prose version of software specifications). These are lightweight formal methods or spec-centric formal methods that don't necessarily require heavy proofs to gain a benefit from them. Since most of the errors I've encountered fall into two camps: straight up logic errors (verification should catch) and specification errors (validation should catch). My focus has been on the latter. I think testing in general catches the former pretty well, or using a language that lets you code out a lot of logic errors, but specification errors are hard-to-impossible to catch until you place the product in front of the customer. Applying formal methods + simulation & modeling to the specification can really help here, even if it's only to subsets of the spec, as you can test against that verified/validated specification more effectively than against a prose specification (what I usually see in my work, 1k+ documents that are largely self-contradictory).

3. See 1. I did that on my own, but it was intended to start a conversation in the office about modeling our systems more formally to gain similar insights elsewhere (and better understand the system design). It did not take off.

4. People don't want to learn the methods, especially in legacy systems (which I demonstrated at my previous office would benefit from formal methods). There's also confusion over what formal methods bring you. I had to repeatedly state that I wasn't going to prove that our system worked correctly (in the sense of proving theorems about the code or something), but only properties of the specification (which for most systems were 1k+ page documents). Without a compelling case study, you will not convince a harried office that it's worth investing in something that seems slow ("Why aren't you coding!?!"), even if it does ultimately save time (once you start coding you can more directly implement the feature or have a better idea of what/how to test).