Ask HN: Why don't you use formal methods?
4 comments
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.
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 you've hit the problem of "why it isn't adopted" really well. Most people seem to have learned formal methods as "prove this source code does exactly what it should based on the spec", but formal methods don't have to apply at just that level.
Formal methods can be applied at the specification level, instead. This can be much simpler as you get to ignore a lot of extraneous details. This is also important because many real-world problems are not because the code is implemented correctly, but because the code implements a bad specification (the spec doesn't do what they think it does).
Using something like TLA+ or state diagrams or other things which can be executed (in a sense), which are formal representations of the specification, you can find the issues in the specification before you even touch the code. I've also used it as a way to "debug" by taking the ideal, creating the spec and showing it does work correctly, then weakening the constraints in the model until it behaved like the implementation, which gave an idea of where to check in the implementation (which found the problem, but was hard to debug because it was an embedded system).
A (more) concrete example: We had an embedded system with multiple nodes running internally and concurrently that communicated via a shared memory system. You may have already guessed that this could lead to race conditions, and that's what we found. But in trying to sell TLA+ to a colleague, I showed a model of how they were using the system for a part that was constantly giving them errors. We were able to create a much simpler model than the code (which had become several thousand lines in each of two nodes). The model was maybe 100 lines long and focused strictly on how they communicated. We dropped out the message contents (irrelevant) and only modeled the size (variable, but we simplified to 1-10 or something like that) and the buffer size (for the model this was configurable) and the list pointing to where in the buffer messages started (list length was configurable), and a few other details. In making the specification it became clear where the problem was and we didn't even have to run the model checker.
If they'd started with modeling that specification more formally (what they had was all prose and tens of pages long in two specification documents), they would've saved months of headaches cleaning up the numerous issues with it.
Formal methods can be applied at the specification level, instead. This can be much simpler as you get to ignore a lot of extraneous details. This is also important because many real-world problems are not because the code is implemented correctly, but because the code implements a bad specification (the spec doesn't do what they think it does).
Using something like TLA+ or state diagrams or other things which can be executed (in a sense), which are formal representations of the specification, you can find the issues in the specification before you even touch the code. I've also used it as a way to "debug" by taking the ideal, creating the spec and showing it does work correctly, then weakening the constraints in the model until it behaved like the implementation, which gave an idea of where to check in the implementation (which found the problem, but was hard to debug because it was an embedded system).
A (more) concrete example: We had an embedded system with multiple nodes running internally and concurrently that communicated via a shared memory system. You may have already guessed that this could lead to race conditions, and that's what we found. But in trying to sell TLA+ to a colleague, I showed a model of how they were using the system for a part that was constantly giving them errors. We were able to create a much simpler model than the code (which had become several thousand lines in each of two nodes). The model was maybe 100 lines long and focused strictly on how they communicated. We dropped out the message contents (irrelevant) and only modeled the size (variable, but we simplified to 1-10 or something like that) and the buffer size (for the model this was configurable) and the list pointing to where in the buffer messages started (list length was configurable), and a few other details. In making the specification it became clear where the problem was and we didn't even have to run the model checker.
If they'd started with modeling that specification more formally (what they had was all prose and tens of pages long in two specification documents), they would've saved months of headaches cleaning up the numerous issues with it.
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.
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).
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).
Some specific questions I'd be really interested in hearing answers to:
* Have you ever used formal methods outside of your professional life (e.g. in personal projects, in a previous academic career)? If so, what methods did you use, and what did you use them for?
* Do you think your professional work would benefit at all from the use of formal methods? Why/why not?
* Have you ever used formal methods in your professional work? If so, what methods did you use, and what did you use them for?
* If you have never used formal methods, do you perceive a significant barrier that prevents you from using them (applicability issues aside)? If you have used formal methods, do you see issues which prevent widespread adoption?
(I mean you specifically; I've read some of the many articles which give varying explanations on why formal methods have never taken off in the mainstream.)