Formal Methods: Just Good Engineering Practice? (2024)

It hasn’t been my experience that it is as niche as this. I believe the “costs,” people refer to in these discussions have come way down over the last couple of decades. I’ve taught developers how to use tools like TLA+ and Alloy in week.

It’s not a skill that requires a PhD and years of research to acquire these days.

Nor does writing a basic, high level specification.

If anything you will learn something about the system you are modelling by using a model checker. And that can be useful even if it is used for documentation or teaching.

The fundamental power of formal methods is that they force you to think things through.

All too often I find software developers eager to believe that they can implement concurrent algorithms armed with their own wit, a type checker, and a smattering of unit tests. It can be humbling to find errors in your design and assumptions after using a model checker. And perhaps it’s hubris that keeps programmers from using such tools in more “mundane” and “real world” contexts.

There are a lot more “small” distributed systems than you’d expect and state spaces are generally larger than you’d anticipate if you weren’t open to formalizing your work.

It’s not all or nothing!

I work on a very “product-y” back end that isn’t fully specified, but I have formally specified parts of it.

For instance, I property-based-tested a particularly nasty state machine I wrote to ensure that, no matter what kind of crazy input I called an endpoint with, the underlying state machine never made any invalid transitions. None of the code around the state machine has a formal spec, but because the state machine does, I was able to specify it.

In the process, I found some very subtle bugs I’d have never caught via traditional unit testing.

"Formal" means "written in a language that can be interpreted by a computer" and that is the very thing programmers do. Writing a code is writing a formal specification of the program's behaviour, and by definition, every piece of software must do that.

But you're right that to benefit from any formal methods, you need to compare the program's behaviour to something else that isn't the program itself, and that other thing also needs to be written in a formal language. To be able to write that other thing, you do need to have a precise understanding of what the wanted behaviour should be so that you could express it in a formal language, but it doesn't have to cover the full behaviour of the software.

As an example of what that means, take automated (unit) tests. Automated tests are a formal specification, and running them is a formal verification method. Tests are a relatively weak specification, and executing them is a relatively weak verification, compared to what we normally mean by "formal methods", but there is no clear qualitative difference -- conceptual or even practical -- between tests and more powerful formal specification and verification. You can think of these practices as more powerful tests or as tests that work differently, but tests are formal specifications, and if they're applicable to a piece of software, it's likely that richer formal specification methods are, too (learning the cost/benfit of other methods is similar to learning the cost/benefit of tests -- you don't get it right at first, but you learn along the way).

You are going to have requirements whether you like it or not. It doesn't matter if you discover them during requirements engineering and validate and deconflict them on a simple text document, or if you discover them as you go during coding (possibly after having coded the wrong thing), or if the client discovers them during the "sprint review" of some allegedly agile cult. The only difference is how much money and time are you willing to trade for being called "agile". Ironically the traditional way of doing a requirements stage is the less expensive of all three options. It is also the most aligned with the original agile spirit, since it converges with the client as soon as posible, at the point where changes are the most cheap (changing a line on a text document).

I think it's more formalisability than requiring upfront design. For example you may have an insurance claim automation system which you can't design upfront because most insurance providers have unspecified behaviour. But that doesn't mean you can refine your automation system as you get more information from interactions. You would still get the benefit that you ensure not leaving out any cases or not having any contradiction in your system

Formal methods for critical systems totally make sense.

Formal methods outside of that are just silly. You can prove your software meets some spec, but the spec will always be wrong. Either it’s wrong today because it’s incomplete or you misunderstood something, or it’s wrong tomorrow because systems constantly evolve at high speed.

I feel like the silly absolutism of formal methods folks held back software development as a field, what we needed was practical methodologies to reduce bugs and accelerate development not philosophical waxing about “correctness”, a concept which does not exist for most software.

Fortunately I think we’ve mostly moved on now, and there has been great work on testing, language design, methodology development, that has had real impact. The sheer scale of available software and how incredibly reliable it is, has made formal methods irrelevant to mainstream software development.

Static type checking is a kind of formal verification of software - there are formal requirements (the program doesn't go "wrong" in a number of rigorously defined ways) that are automatically checked. And you can certainly do "design and development" together in type-safe languages.

That’s true. Back when they were inventing security, the requirement for high-security systems (A1 under TCSEC) required formal verification. Those who did it said its cost ranged from not too burdensome to very high. What’s the reason?

While many requirements existed, the design assurance required specifying what problem was being solved, how it’s being solved, and the safety/security properties. Then, proving that the security properties were embodied in the artifacts in all states. That problem is difficult enough that most people who succeeded were also geniuses good at programming and math. Geniuses are in short supply.

The lessons learned papers also pointed out a recurring problem. Each requirement, security policy, algorithm, etc needed a mathematical specification. Then, proof techniques were necessary that could handle each. Instead of developing software features, you are now both developing software and doing R&D on applied mathematics.

Steve Lipner’s The Ethics of Perfection pointed out it took several quarters to make a major change on a product. The markets value development velocity over quality, even demand side. So, that’s already a no go for most businesses. Likewise, the motivations of OSS developers work against high assurance practices as well.

If you want formal verification, then you are forced to make certain decisions. For one, you need to build simple systems that are easy to verify, from design to language. Then, you use the easiest, most-automated tools for the job. Most drop full verification to do automated, partial checking: TLA+, Alloy, SPARK Ada, Meta’s Infer, etc.. If doing full verification, it’s better to make or build on reusable components like we see done with CompCert and seL4. GEMSOS and VAX VMM advocated that back in the day, too.

So, most software development isn’t fit for use of formal verification. I think we can default on a combo of contracts (specs), automated testing, static analysis, and safe languages. If distributed, stronger consistency when possible. Then, use CI to run the verification on each commit. Some tools can generate patches, too.

IMO UML is useless because whatever diagram gets produced means different things to different people and it's very complex but not check-able so people can make UML diagrams that are self contradictory or nonsense.

I find myself using a "method" of some kind when faced with a problem that's hard to think about. A communications protocol - nice to have a state machine to describe it for example. TLA obviously fits that niche even better. I've been lucky enough not to have too many problems recently that felt like they justified that effort but it's of incredible value when one does. Domain Specific Languages - so much better to use a parser framework than hand-code if you want to avoid all sorts of undesirable outcomes.

Currently most of my rework comes from changes to the requirements and our "customers" not really knowing what they want till we give them something and they say "not that."

This is partly because the people asking for things don't fully think out all the implications of what they're asking. It's mostly about not having enough knowledge in one place to make good decisions on.

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

My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for.

Formal methods are a large investment, too. No two ways around it.

Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.

I only am familiar with formal verification in the context of a hardware class, which is like programming but the cost:benefit is wildly different (can’t fix a physical chip after it has been fabricated very easily) and the types of designs are very different.

But, the impression I got was that the rigors of the formal verifier would sort of impose a limit on the complexity of the design just based on… completing in a reasonable timeframe and in a reasonable amount of memory space. Maybe the true victory of demanding formal verification would be fixing:

> software is big and complicated and hard to get right

By making big complex programs a pain to work with, haha.

If we’re going to boil this frog, we need to steal wisdom from TLA, not teach it. Type systems have borrowed a lot from Hinley-Milner, and are themselves a formal, partial proof.

I think I’d like to see a descendent of Property Based Testing that uses SAT or TLA techniques to rapidly condense the input space in a repeatable fashion. We should be able to deduce through parsing and code coverage that passing 12 to a function can never follow different branches than 11, but that -1 or 2^17 < n < 2^32 might.

> if it was really that helpful, more people would be applying it and the benefits would speak for themselves

Well... that's not a good logic on any area, and on software development it's twice as bad.

Most software projects still fail. And that's not "market failure", it's just "didn't manage to build it".

UML is far more useful than TLA+, at least from the point of view of agile delivery projects.

Starting by at least with UML everyone, regardless of their role, can have some kind of understanding of what those diagrams are about, and UML covers most scenarios from software delivery product lifecycle.

Whereas TLA+ is mostly abstract code that after proving a specific algorithm is right, has to be manually ported to the actual software development stack being used, with the caveats a manual translation implies, and only applies to algorithm logic, nothing else.

UML has a place at my work, TLA+ will never get one.

For Calculus you can easily explain to the unenlightened that many physical and engineering laws work in terms of speed and acceleration of measurable values, and Calculus is a mathematical framework for working with this.

TLA+ and the like work because they target a very small specification language.

With the large footprint of Rust, I've seen questions raised about how this will work. But haven't seen good answers.

Would love to read more.

I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.

> Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand,

I actually generate a unit tests with LLMs a lot lately. They do a decent job and you can just ask it to be a little more exhaustive, test any edge cases it can think of, or instruct it to deal with specific ones. I know a fair bit about how to write good tests and the effort you can put in that. But LLMs can generate better tests than me way faster.

If anything, they are less likely to do a half-assed job of it than me because I tend to run out of patience doing repetitive tedious shit. This is a healthy trait to have for a software engineer: we are supposed to make stuff easier by automating it. If it feels repetitive, your reflex should be to write code to make it less repetitive. Documentation is the same. I generate that too these days and since it is so easy, I do it more often and sooner.

LLMs might trigger a minor revolution in the adoption of formal method verification. Generating a correct specification is a combination of tedious and probably relatively easy for an LLM given enough context like working code, documentation, and other hints as to what the thing should do.

I'd be a lot more likely to bother with that stuff if I can just let it generate specification and then briefly glance through them than if I have to spell everything out manually.

I think using Rust kind of signals that you care about correctness. It's compiler is probably the closest to proving your system is probably correct that you can get without resorting to formal methods. And probably a lot easier than trying to bolt on formal methods to languages that don't even use a compiler or explicitly specified types.

Yeah but proptest / qcheck is not formal methods at all. It's randomised testing.

Have you tried FizzBee.io? It has a python-like syntax. Take a look at the example. https://fizzbee.io/examples/two_phase_commit_actors/#complet...

Formal methods don't have to be complex. The issue is, most formal methods are designed as an academic exercise to demonstrate a specific topic the professor was interested in. (Or TLA+, that was designed specifically for writing papers)

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

It looks scary but actually all those concepts are really simple and probably things you are already familiar with.

A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces.

Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).

Thanks! Macroexpanded:

Formal methods: Just good engineering practice? - https://news.ycombinator.com/item?id=40753989 - June 2024 (149 comments)

15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - May 2024 (1 comment)

Thanks, I couldn't find it via Google search on this website for some reason.

Arguably, if 'real' Agile is ever found Formal Methods would be the antithesis of it: something provable and reproducible is blasphemy to True Believers.

How about https://en.wikipedia.org/wiki/SPARK_(programming_language)

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

That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements.

The other way around (verification of program with respect to the specification) can be more feasible to implement.