Formal methods: Just good engineering practice?
brooker.co.za
brooker.co.za
Formal methods need to be like SPARK 2014, or DbC, actually part of the programming language, or being able to generate code in the target language, interop with its libraries ecosystem, and have good quality good with performance, that won't make people want to remove the generated code and rewrite it manually.
Some fp languages are close enough to fit that bill; Rust too is going down this path: its type system was built to make a proof, after all.
But TLA+ is a bit of an unusual proof language. I think most of them are like you describe: SPARK, Dafny, F*, CBMC, all the Rust ones, etc. I'm not sure about the interactive proof languages (Coq et al), they are too complicated for my normal sized brain.
I wouldn't think I need to explain this to a professional developer, if you are waiting for the silver bullet that solves all your problems you may as well go take care of goats.
Yes, we should be open minded, and the tools should also be improved so that developers on the trenches bother to learn and use them.
EDIT: There was an edit adding the final part of the comment after I submitted mine above. Here is my response to the last part, since the comment was toned down a bit:
Yes, we need to improve the tooling, and TLA+ can be improved a lot, I'd love for it to be able to reason about my code and to have an easier bridge between both words. However engaging in the discussion of how it can be improved without acknowledging what good and usefulness it brings is just not useful in general, and it just puts off people that could benefit from it from ever using it.
TLA+ has a lot of value in some cases, and we should be acknowledging that!
At least now you know it's just bugs you need to fix, and not a faulty logic to begin with.
Managers don't want that though, for reasons that already Dijkstra has outlined.
Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).
Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.
As everything it is a tradeoff, a lot of things do not deserve a proof, but for the ones that do you are a lot more productive.
It also depends on the level of the proof, I want to make sure the idea is valid and it takes some time to know what to abstract and what not to (it is a model after all). So if you are aware of what you are testing and at ehat level the tool and your proof is working it is very beneficial
So closely, that when you transcribe such an algorithm to C, there is very little room for error, even if the C code isn't proven directly.
Can you list some/all of them please? Would be helpful to others here.
So true, but you know what would be amazing and useful? A TLA+ spec transpiler that emits fuzzing code. That would probably be easier to make than TLA+ spec transpiler that emits C.
With e.g. the C bounded model checker CBMC, your model language is also C. Frama-C is another approach (Hoare-like, axiomatic logic). Klee works on LLVM IR etc.
Stronger proponents would perhaps suggest extracting the implementation from the model etc., but you don’t have to drink all the koolaid at once to get many of the benefits.
And not all your software needs to be formalized either, to get many of the benefits.
I’ved succesfully used CBMC and Klee on C code for verifying important parts of embedded safety/mission critical software on resource constrained HW (i.e. no OS, static allocation, single to double digit kilobytes of RAM etc.)
Formal methods rock!
This sentiment is sloppy, dismissive, with an tinge of obligation to bend to old man wisdom. I don't buy it for a moment.
Let's do better.
Formal tools help suss out requirements solved with high level algos for selected hard sub-issues of the problem under consideration. It's not code to be sure. And, this argument cuts both ways.
It's also far from a clear a pile of code knows, expresses, implements, or communicates its requirements. Just because the code compiles doesn't necessarily mean squat either.
So first thing: specification and implementation are both important and walk hand in hand. How tightly you hold onto one or both depends on several factors such as: are you competent in formal tools (learning them is tough), are there really hard sub-problems e.g. distributed computing on the table? etc.
Second, I want to deal with risk ... you know ... connecting the dots end-to-end in software from customer to requirements to coded. I'll motivate my point with a imaginary story.
In Silicon Valley two companies A, B on opposite corners of the same block are having a big team meeting. The big boss is in with important news.
Company A: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. All team leads and lead techs are required to meet with business to assess work planning, risk, task order, deliverables, and so on. We expect this work to run for 18 months. In that time we may abandon, re-prioritize, and clarify work as coordinate with the customer. The customer may change their mind etc.. But as we know well, coding the product goes hand in hand with risk, discovering clearer requirements, and doing a better job of delivering them. We're equal to it.
Company B: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. Part of this new work requires us to glue feedback from three controllers, plus sensors in realtime to compute steering commands to the cockpit console. If we nail this, there's 100x more work for us. Given how crucial this aspect is, we'll use Lean, Spin to model requirements and work out some LTL to make sure we're on the right path before we code. We expect this work to run for 18 months minimum. In that time we may abandon, re-prioritize, and ....
Now at this point the boss at company B is cut off with a bunch of whining from its developers:
* formal live in another dimension
* a good model doesn't mean right requirements
* even if the model is right there's no proof it's implemented right
* it'll take longer to do because we've added scope
* etc..
The boss at company A, B are both doing the right thing. Both companies have risk - a lot of it. But company A has engineers on staff who are preternaturally good at dealing with risk. Company B, unfortunately doesn't really understand risk at all in terms of doing something about it.
In this story company A never talked about formal tools. That's on purpose. I want to emphasize only that the problem to be impacted is risk levels, risk location, and sensible ways to manage it. Here formal is but a tool. It's not magic. It's just a tool. Had the boss at A mentioned formal tools, engineers would have rolled with it seeing it as one more bullet in their armory.
“It would be well if engineering were less generally thought of, and even defined, as the art of constructing. In a certain important sense it is rather the art of not constructing; or, to define it rudely but not inaptly, it is the art of doing that well with one dollar, which any bungler can do with two after a fashion.” Arthur Wellington
For me, engineering is applied science for money. That's the main thing. Someone is paying for everything you do.
We get into it because we care about the how more than the why, but we end up having to deal with the who is paying for this.
The boundary is fuzzy, engineering is heavily influenced by finance, otherwise it's just a hobby.
Formal methods are great or an awful decision depending on wether or not they make economic sense for your product or service at your organization's current stage.
Amazon EC2? A large, mature org, with products with extremely high fubar potential? Go wild.
Your startup where market-fit is not proven? WTF? Are you high? use that money on something else.
It's like unit testing, it in general makes great sense if the cost of maintaining the tests is lower than the opportunity cost of slowing down. If you're prototyping something that you'll likely throw away, it may be a bad idea. Once it proves value, you better build a decent test harness.
Startups take technical debt because it's cheap when the market fit is not demonstrated (you pay it back later once you have succeeded somewhat).
It's a rational decision.
You don't need perfection if you're building the wrong thing, first you figure out if what you're building makes sense, then you decide in what to invest.
On the other hand, if you're building a deep space probe, a large scale distributed system for hire, or any other thing were a failure is BAD (with capital letters), the extra cost of ensuring correctness is well worth it.
This rings true for me. I'm interested in learning things, e.g. how processes work in Windows NT kernel, or how to write a custom memory allocator, instead of creating a product. I do have some passion for a certain product but it is highly personal and won't be shared.
Quoting David Cutler, "What I really wanted to do was work on computers, not apply them to problems". I wish I knew this when I was younger.
I thought that was science, not engineering! Money determines the subjects researched, how they're researched, and the results, right?
It's possible to get funding to research something completely bonkers, in engineering it's less likely.
Now if you can't externalize the costs of catastrophic failure, that will be the fundamental constraint on your engineering / finance strategy. If you really don't want your network to be breached, you'll build it around security features, not try to hack them on after the fact. I like to think SpaceX, as a private company without the kind of political heavyweight backers that ULA enjoyed, thus put a lot more effort into avoiding the kind of problems ULA is currently having, for just that reason.
Conclusion: take away the government safety nets, and both engineering and finance will perform better? Now about Silicon Valley Bank...
But in some sense, many ancient engineers had to drastically overbuild their bridges and other structures because they didn't have the tools to know what the "barely stands" threshold was, so they had to build for a big margin of error when they lacked the tools of precision.
It is not scalable, but the quality is quite stable across batches
> https://en.wikipedia.org/wiki/Pantheon,_Rome#Structure
> The stresses in the dome were found to be substantially reduced by the use of successively less dense aggregate stones, such as small pots or pieces of pumice, in higher layers of the dome. Mark and Hutchison estimated that, if normal weight concrete had been used throughout, the stresses in the arch would have been some 80% greater. Hidden chambers engineered within the rotunda form a sophisticated structural system.[55] This reduced the weight of the roof, as did the oculus eliminating the apex.
That said, I'm guessing the Pantheon is in one piece (unlike the coliseum) because it's been used as a church for the past ~1600 years and presumably (similar to Notre Dame) it gets repair as-needed.
It takes the engineer to build it so that every part is 1.25X as strong as it will ever need to be, consistently everywhere.
To the idiot, that then looks like it is barely standing, because some parts are 4X weaker than he would have made them, based on bad intutition.
e.g. building a bridge to support a city's normal traffic density, but the city ends up growing, and the way the bridge was designed makes adding reinforcement difficult. Or building a bridge whose materials start to melt at a certain temperature that's above what's expected for the region, but climate change raises the temperature over the threshold, so it needs a completely different material.
Hence the article's point that software companies should invest in formal methods, because while formally proving something is a long process without much reward in the short term, it eliminates an entire class of bugs which, in some long-term projects, makes it worth the effort.
We know that’s true experientially in both CS (YAGNI) and in the physical spaces (eg Wright brothers constantly iterating with cheap prototypes until they figured out something that worked and SpaceX doing similar things with their prototypes). Iteration = learning. In theory formal methods let you iterate at a cheaper phase of the project. In practice, the methods themselves are very difficult to scale to large projects and these days require you to build the project twice - once for the formal language and then hand-translated to a production language.
I think of engineering not just as designing and building things, but also knowing where the limitations are of the thing you're constructing, whether it's purely on paper, in a computer's memory, or from brick and mortar.
No, it is worse than that. There are people who claim the proof is the code itself. Just look at it. These are the same kind of people claiming good code needs no documentation.
That is like a bridge engineer saying they need no structural calculation because the stability of the bridge is obvious to a certain kind of bridge nerd if they look at it. Only that civil engineers figured out after a few high profile bridge collapses that "trust me bro" isn't good enough and software engineering people are still in the: "trust him, he is a genius"-phase of the field.
Yet this is what emerges when you write a sufficiently detailed proof.
The more detail you add to your TLA+ model, the more it looks like just another implementation (albeit untyped, so it's pretty easy to slip errors into).
In the end all security measures are a layered effort and doing a bit formal verification, a bit unit testing, a bit fuzzing etc. is always better than mentally aiming for 100% and not doing anything at all.
The question regarding formal verification is: What is the code that is running in the critical domain? Someone who writes safe code will try to minimize the amount of code/executables/complexity in that space. And that domain isn't necessarily a single process, it can be a part in the code, or a process until it dropped privileges etc.
If all your code is critical domain it either means you failed to sanitize inputs, everything runs with yolo/root privileges, all of your customers share a single table in your database, your hardcoded admin password is 1234 — or maybe you write code that controls nuclear power plants, airplanes or similar things. But if it is the former, no amount of formal verification will save you anyways because wrote software like a money writes poems: By accident.
If the idea of a critical domain is new to those reading this comment, if you never thought about user proviledges when writing an application, please read this as proof of the point that the field of software engineering still lacks in all sort of places and it is in all our interest, both professional and as users/potential victims to improve the situation.
Granted. But engineering is about making sure we don't make mistakes and just like in math class a good way to assure that is to take two different paths and arrive at the same place.
Arguably, software engineering does this much more exhaustively then any other engineering field... To very varying quality output, from masterpieces like SQLite to your average B2B artifact which barely works despite having 99% coverage.
If you manage to solve the halting problem first.
Adding annotations to the code for example is not a workaround for the halting problem.
(Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).
So yes, it is all about push button technology here. If you are willing to put in the work to write down the proof yourself, instead of expecting a magical entity to generate it for you, then it is possible. All the halting problem says is that there is no such magical entity. You will need to know why your software is correct.
The vast majority of loops iterate over some finite collection of elements and are thus guaranteed to terminate. Tricky cases are stuff like "I will repeat this operation until the output stops changing".
If you're making Space Shuttle software from scratch yes. In practice for 99% of current mainstream development you depend on piles upon piles of dependencies, which might or might not check those loop invariants correctly, or might have a (trivial to add) endless blocking timeout, a deadlock, and many other wonderful things.
Usually they're not even set in stone, you'll update to the next version, and if they introduced such an issue, there's lots of fun to be had.
Nobody doubted you can have formal proofs for algorithms, or checked software in certain conditions and for certain controlled environments (e.g. using MISRA C and such) (in fact, I support this in a comment elsewhere in this thread).
The objection is to the idea that this is applicable (or trivially applicable, and we just aren't doing it out of laziness or something) to regular software development.
Continuing the stream of inputs holds no meaning once you've tested every possible permutation (branch coverage) beyond checking for memory leaks. Every software has a finite amount of states it can hold, most developers just erroneously expect some states to be unlikely or impossible to reach.
there is a large slice of algorithms, which are possible to prove that they are not affected by halting problem. I think having tooling for this slice of algorithms is already a big win.
Is exhaustive testing even possible in theory?
What you're asking for is literally only possible in theory and entirely pointless in the context of reality, because you cannot guarantee that a device is available at runtime, invalidating any proof. The same applies to any engineering projects, software or otherwise
if (x > 0) {
/* code */
} else {
/* more code */
}
Given your example no software can ever handle this equation given infinite numbers, as all CPUs have a maximum number they can compare.
Just like you cannot prove that a bridge will be able to handle a given load. Engineering fundamentally can only make assurances within expectations. Your tests define these expectations, and by covering 100% branching coverage you've exhaustively explored all valid states your software can have.
Do note I'm talking about actual 100% branching coverage here, not just 100% coverage of your own code, ignoring libraries and runtimes you've imported. That's way harder then you seem to think and the reason why sqlite (the linked page) has so much more testing code then application code
loop { if (A) { ... } if (B) { ... } }
100% branch coverage means you've encountered both cases, but the loop could have encountered these in any number of ways specifically this branch could be encountered as either A && B both A && !B && B && !A, all of them exhaustively, and could even depend upon whether the order branches were taken matters.
While formal methods give an exhaustive proof.
No, it doesn’t.
bool is_even(int n) {
return true;
}
bool test_is_even() {
return is_even(2);
}
Your example software makes the claim that integers that the given runtime/interpreter/VM can handle will be assured as true. This was tested.
Nobody said that any description of the software is always correct, just because a test was added that tests random stuff
Also note that that's not 100% coverage. It merely covers your code, which builds upon other code.
Feel free to actually read the given link. Your horizon might be expanded. Or don't, and keep your dunning kruger worldview
Tests proof that something can handle the exact scenario that we're testing. The forces on a software system are just different and in some ways less predictable than for e.g. a building. But in software the consequences of failure are often less catastrophic[1] and it's a lot cheaper to run a battery of tests.
[1] And if they are not less catastrophic than a collapsing building, you'd better test it far more extensively than an average system. That's engineering too, making a trade-off between the costs of failure and the cost of preventing failure.
Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds.
Meanwhile almost every medical device under the sun today has software, nuclear powerplants run on software, space missions use software, airplanes drive themselves and land through software, etc.
For software that really matters you have standards like MISRA C you also have professional bodies like IEEE, ANSI, you have ISO standards for software development and infrastructure, there is a lot of standards and regulations that you can follow just like in all other fields. There is NIST for security and I could probably go on and on. So it is not "overcomplicated hand-waving".
But no one is going to deal with "implementing formal approach" for "yet another crud app", they will hire whizz kid who knows latest JS framework and be done with it paying him 1/10th of cost of someone who knows more than that.
That seems obviously false, unless you understand ""proof"" in such a lax manner that software engineering has them as well.
I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment.
TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.
There are plenty of canonical examples out there for resolving some issues with types, and having a bunch of one-pagers on issues people hit that people might or might not want to tackle with some flavor of formal method.
There are some complexities, to be fair, but these are mostly around the performance of the model checker. Some things are easy to check, and other things, like loops and recursion, are harder to check. However, this is a matter of optimization, and with practice, this becomes quite easy to deal with.
It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.
I'd wrap libraries that were problematic to build function contracts around before I punted on model checking. Hell, I'd fork and refactor these APIs to work with lightweight fibers before I gave up on model checking. The utility of something like async / await is small potatoes compared to the utility of having code that has even light formal verification in place.
For instance, in electronic engineering, you don't use the most accurate model of a diode at all times. Sometimes it's just a one-way valve. Sometimes, it's just one-way valve with a 0.7V drop (if silicon).
In mass production, you will not get the accurate parts needed for the most formal model to be justifiable, and the cost of those parts would not be justified in most of the circuitry.
It sounds to me like you have a philosophical problem with LLMs, which is something I don't think we can debate in good faith. I can just share my experience, which is that they are excellent tools for this kind of thing. Obvious caveats apply - only a fool would rely entirely on an LLM without giving it any thought of their own.
Sounds like it could be a good starting point for something like this.
As I see it, the only way to do it properly is to embed the proof in the code like we embed types in the code. For example, we've been able to get rid of NullPointerException completely by using the checker framework, all we need to do is maunually annotate all values that may be null (everything else is assumed non-null, if you try to assign it to null the compiler won't compile):
@Nullable String getSomething();
I even played with adding support for dependent types, I am convinced the compiler extension would allow me to do that, but unfortunately I have other things to do.
They made really, really good hardware, but it was extremely painful for us software schlubs.
That said, I don’t know if it’s really possible to do really big stuff, with a team, unless you have some degree of formality.
Best practices are usually a good place to start, and I would suggest that the degree of necessary formality, is inversely proportional to the experience of the team. If you have a lot of really experienced engineers, in a mature team that has been together a long time, the formality is still there, but doesn’t need to be written down.
I usually work alone, or as the sole technical person, in a diverse team. I’m really experienced, and don’t write much down.
But I’m also really, really formal. It just doesn’t look like it.
But I do spend a great deal of time reviewing my work; often going back, and tweaking and testing, for days.
My testing code tends to dwarf my implementation code.
The main issue is that we can get so wrapped up in the process, that we fail to get anything done.
It’s a question of balance.
My hope is that code assistants can make all this much easier by facilitating synthesis, you write the specification, and ML gets you the code. I have a fairly good toy prototype doing such a thing for the subset of a common functional programming language. Obviously, the difficulty is to scale it and make it practical.
It’s funny, but there’s a heck of a lot of structure, in today’s software industry. It’s just not called “process,” or “formal methods.” It’s just “this is how everyone does it.”
Pretty much a requirement, when your workforce leaves, every 18 months.
Think proving your software correct with math, not "project management forces us to write documents".
Formal methods is very much not "how everyone does it", currently.
BTW: that corporation was very much into “proving right with math.” The Japanese really like math, and this corporation probably has hundreds of patents, describing testing and validation methodology.
Watts Humphrey once wrote a book that described a personal formal methodology. Can’t remember the name, but it was a really big deal, in the 1980s. I think it went a bit overboard, but it worked well, for folks that followed it completely.
Humphrey's Personal Software Process is just another project management methodology; nothing do with this topic.
Cool. Have a great day!
I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD.
Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.
I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy.
I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations.
I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.
It's more geared towards the static elements of the system, and writing a spec feels quite like writing a relational database schema -- mostly because they're both expressions of relationships.
It seems like a pretty natural path to write a spec in alloy before building out some crud interface.
I think there's a huge tooling gap though. Alloy, TLA+ and friends all seem to be very jvm/UI centric, really targeting a user who is working in the editors the language ships with.
I'd really love to see more tooling to run model checkers in a CI pipeline, or generate stubs and test cases for various languages. If that were in place, I think there would be more stickiness to formal methods.
I've started writing a Go parser for alloy, in part to learn it better, in part because I know go and want to write some tooling that I think go would be a good implementation language for. I don't know if anything will come of it, but at least having a parser would allow for things like a formatter or code generator. If I were feeling ambitious, I might try to implement a model checker.
Helpful to escape the alloy UI:
I looked into what it would take to tackle it from the source code, There were some barriers, like the jars not really being published to maven, but the biggest just being the time & energy investment to pick up java again.
I'll definitely be looking into this project and seeing if there's anything I can contribute back.
I came across this when researching/studying Formal Methods but have not yet really sat down and tried it out.
Glenn Vanderburg - Real Software Engineering