Formal Methods: Just Good Engineering Practice? (2024)

brooker.co.za

211 points by aiono 6 months ago


constantcrying - 6 months ago

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.

commandlinefan - 6 months ago

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.

synchronousq - 6 months ago

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].

[1] https://github.com/verus-lang/verus

jcgrillo - 6 months ago

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.

[1] https://crates.io/crates/proptest

IshKebab - 6 months ago

IMO formal software verification is still waaay too difficult to be worth it in all but the most extreme cases. That's really different to formal hardware verification where it is a no-brainer.

I keep trying to learn it, but you need to be a real expert. Like "I wrote the compiler" level expert for most systems.

For example I tried to prove a varint encoder/decoder. It worked for one or two bytes, but not more. Asking for help the reason was that the compiler internally only unrolls loops 5 times, or some random internal detail like that that you could never really hope to know.

I've been learning Lean recently, and ... I mean I like it, but if you learn it you're going to encounter documentation like this:

> Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence.

And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.

charleshn - 6 months ago

On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0].

Basically you just need to log events - which you can even have for free in event-driven architectures etc - and run some predicates on execution traces, e.g. "Always(Locked, Implies(Eventually(Unlocked)))", etc.

One can run it on historical traces, but also couple it to stress tests, fuzzing etc to explore the state space.

Quite simple, powerful and widely applicable, and doesn't require a model, just predicates.

[0] https://en.m.wikipedia.org/wiki/Linear_temporal_logic

ot - 6 months ago

Previous discussion (Jun 2024): https://news.ycombinator.com/item?id=40753989

franktankbank - 6 months ago

Too slow, planning==ossification any documentation can and will be used against you in the Agile court of law.

thefaux - 6 months ago

Most of the articles I've read about formal methods feel like lead gen for consultants. That's fine but feels obnoxious when they implicitly act as though they have reached formal methods induced enlightenment that you can too if you buy a pack of trainings for your employees/coworkers or hire me as an employee to fix your bad (irresponsibly dangerous even!) programming habits.

Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.

jayaprabhakar - 6 months ago

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.

AnimalMuppet - 6 months ago

Good engineering practice is to use the appropriate level of rigor. It depends on what the cost of failure is, and what the cost of the rigor is.

jgalt212 - 6 months ago

If a TLA+ transpiler could emit Python, Javascript, Java, C, Rust, C++, Go (even just one of these), it would be infinitely more usable in that it helps you cross the gap from "I know my TLA+ is correct" to "I know my Go is correct".

Or as a baby step, does TLA+ emit comprehensive test cases? Then we as programmers still have to do the hand transpilation step, but at least we can be assured our implementation is correct (if not efficient).

trending486 - 6 months ago

Modern formal methods like TLA+ and Alloy are as easy to pick up as Python, and other than having to write a spec (an ultra-simplified model of part of a system) they are completely automatic (based on model checkers). There is no reason for a modern software engineer not to have them on her radar. As a matter of fact most of the cloud systems you are using everyday have been verified with modern formal tools: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB, ... and many others.

brap - 6 months ago

I’m not super experienced with formal verification, but I did dip my toes in it a few times.

My impression is that it’s far from a magic bullet. Writing formal specs is basically like writing the code/tests just differently. And the more it covers the more it becomes the same thing. And it suffers from the same problems.

My conclusion every time was that the code itself is the formal spec and the formal spec is the code.

By analogy with construction, the code is both the building and the blueprint.

markusde - 6 months ago

I'd recommend anyone with a passing interest in the role formal techniques can play in software development watch this [1] talk. Mike Dodds is a principal scientist at Galois (a company which has a lot of experience with applying formal methods in industry and government) and the talk does a good job at explaining where they've seen value-added from formal methods, and the right kind of formal methods for different applications.

[1]: https://www.youtube.com/watch?v=gfvvowAc130

nimish - 6 months ago

Formal methods work great when the price of failure is absolute. Mostly pointless otherwise but can be a good exercise I guess.

UltraSane - 6 months ago

AWS has said that when software has a robust set of formal verification tests they can be very aggressive when optimizing it and be confident that they aren't changing its behavior. They say they were able to optimize their IAM authentication code by over 50% this way.

noelwelsh - 6 months ago

I would guess a majority of developers use formal methods these days. We just tend to call them type systems, and for some reason consider them a distinct category. If simulations count as formal methods, then tests, and particularly property-based testing, also make the cut.

Animats - 6 months ago

The article is thin on specifics.

Some problems specify well. A database is an example. A spec for a database can be written in terms of exhaustive search, running the query against everything. Now show that an efficient database yields the same output.

begueradj - 6 months ago

For those interested in the information exchange about this same article: https://news.ycombinator.com/item?id=40753989

- 6 months ago
[deleted]
- 6 months ago
[deleted]
lincpa - 6 months ago

[dead]

linkerdoo - 6 months ago

[dead]