Formal verification of software, as the article acknowledges, relies heavily on the type of software and the development process.
To use formal verification you need to have formal requirements of the behavior of your software. Most software projects and design philosophies are simply incompatible with this.
In software development and design can often fall together, but that means that it is uniquely ill suited for formal methods. If you are developing, before you are sure what you even want, then formal methods do not apply.
But I agree that there are certain areas, mostly smaller, safety critical, systems, which rely on upfront specifications, which can heavily benefit from formal verification. E.g. Aerospace software relies heavily on verification.
One issue with the current proponents of formal methods is, they want to claim others who don't use formal methods as "lazy" or "dumb" and want to claim their superiority because they "do the right thing" and "mastered a complex language".
Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new.
Recent easier to use formal methods:
1. FizzBee (Uses Python dialect, almost reads like pseudo code)
2. Quint: Another formal language with easier to use syntax
3. P: Use syntax similar to C# users.
The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html)
But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.
I see this line of reasoning about formal methods a lot: software is big and complicated and hard to get right... therefore formal methods.
On the one hand, I _want_ this to be true both for selfish and practical reasons: selfishly because I'm very very good at learning things that require an academic learning approach (read a book, work some exercises, practice) and if something I'm good at is important, that means more money for me. Practically because they're right, software _is_ big and complicated and hard to get right and as a practitioner, it's really frustrating when it does fail and I'm scrambling to figure out why.
On the other hand, though, nobody ever seems to make a compelling case for how formal methods proposes to solve that problem. This author actually does better than most by pointing out how most modern "design" is a waste of time but doesn't really go into why TLA, say, is better than (demonstrably mostly useless) UML. There's sort of an implied suggestion that if you dedicate a few months (or years?) to learning TLA, you'll reach enlightenment and understand how it's helpful in a way that's impossible to articulate to the unenlightened. And that's not impossible to imagine! Calculus and Bayesian statistics are kind of like that; you need to really understand them before you can really see why they're useful.
I always find myself left applying what I call "project manager" logic - I need to make a snap decision right now about whether or not I should invest time in this "formal method" stuff or not so I have to be observational: if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.
I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1].
The lightweight formal methods callout is a good one. Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand, but the insights they provide due to extensive coverage and compact understandable failure cases are way better. And crucially this approach does align with normal software development practices.
constantcrying ·6 days ago
To use formal verification you need to have formal requirements of the behavior of your software. Most software projects and design philosophies are simply incompatible with this.
In software development and design can often fall together, but that means that it is uniquely ill suited for formal methods. If you are developing, before you are sure what you even want, then formal methods do not apply.
But I agree that there are certain areas, mostly smaller, safety critical, systems, which rely on upfront specifications, which can heavily benefit from formal verification. E.g. Aerospace software relies heavily on verification.
Show replies
jayaprabhakar ·13 hours ago
Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new.
Recent easier to use formal methods: 1. FizzBee (Uses Python dialect, almost reads like pseudo code) 2. Quint: Another formal language with easier to use syntax 3. P: Use syntax similar to C# users.
The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html) But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.
commandlinefan ·6 days ago
On the one hand, I _want_ this to be true both for selfish and practical reasons: selfishly because I'm very very good at learning things that require an academic learning approach (read a book, work some exercises, practice) and if something I'm good at is important, that means more money for me. Practically because they're right, software _is_ big and complicated and hard to get right and as a practitioner, it's really frustrating when it does fail and I'm scrambling to figure out why.
On the other hand, though, nobody ever seems to make a compelling case for how formal methods proposes to solve that problem. This author actually does better than most by pointing out how most modern "design" is a waste of time but doesn't really go into why TLA, say, is better than (demonstrably mostly useless) UML. There's sort of an implied suggestion that if you dedicate a few months (or years?) to learning TLA, you'll reach enlightenment and understand how it's helpful in a way that's impossible to articulate to the unenlightened. And that's not impossible to imagine! Calculus and Bayesian statistics are kind of like that; you need to really understand them before you can really see why they're useful.
I always find myself left applying what I call "project manager" logic - I need to make a snap decision right now about whether or not I should invest time in this "formal method" stuff or not so I have to be observational: if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.
Show replies
synchronousq ·6 days ago
[1] https://github.com/verus-lang/verus
Show replies
jcgrillo ·6 days ago
[1] https://crates.io/crates/proptest
Show replies