That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...
Think about the filesystem, the big issue with formalizing a program spec that operates on a file system is simply the fact it is essentially a shared object amongst all the programs running on the system. Add to that the fact that (though this changes with modern containerization systems, namespaces, pledge what ever) a program may at any point gain access to root permissions if it makes the system call to do so providing the correct credentials it becomes very difficult formally be able to remove any possible states from the system.
All this could be different but we would radically need to redesign are systems and the way we think about the problems.
Where do you start for formalizing this?
An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write.
Yes, that's the kind of contract we take on regularly. My point is that the exact thing the customer wants/needs is the one part that can't be formalized meaningfully - it's good when we show them something and they tell us is good. Everything else doesn't matter - could be the worst UI, maybe you have to reboot the computer once before starting it and once after exiting it, maybe it leaks enough memory that you have to reboot every day anyways - what matters for them to pay you is "do they like the drawing quality" and really nothing else
This indeed could not be formalized by it's very nature. I was not making a claim on the applicability or even the desirability for all programs and I think many people who have not look at it properly overestimate it's applicability.
What I was trying to say is for the subset of programs that one would want to formalize (such as the examples I gave) the task could be much easier if we have formal primitives, including operating system primitives and networking primitives to provide guarantees.
My other point would be that a lot of developers and projects are writing code that could potentially prove properties and benefits could be derived from proving these properties. I would look at middleware programs as some of the obvious ones that could massively benefit from such techniques and formalization (though things like streams can be much more easily formalized and modeled correctly).
I think that's fine though. The exact fuzzy thing the customer wants is typically still built on top of a ton of stuff that can be verified. I'm not sure it needs to be either-or. You formalize what you can, and do your best with what you can't. Ideally (if we could find a way to make formalized software cheaper/easier to build) it would reduce time wasted on the stuff that can be formalized, and allow spending more time on the stuff that can't be.
It's absolutely not impossible to simply add one more layer in-between the developers "drawing the rest" and delivery. They just not formalize it as software in one go, but "in two".
OTOH, we can probably call a much less formal spec good enough. Just that it doesn't write past the end of buffers would be very helpful. We can also throw a bounds in - if we can't prove it in X iterations then call it false (expect to adjust X to very large)
What I was trying to show is the nightmare of modeling accurately and in a way that matters lots of operating system primitives and further reasoning about when the assumptions have been violated by the program set up.
Indeed this does not effect the stuff outside the interaction of the program with the operating system and my point when it came to modern programming primitives is that not all data structures or methods of programming lend themselves to being able to write formal proofs about them.
You might be able to have a type BigInterfaceTypeThatDoesLotsOfThings<a> but this might be impossible to formalize in any meaningful way and AI is not the panacea and this stuff is not easy and require hard thinking.
Additionally a lot of formally verified programs are done via constructive proofs where you build up the correct program from primitives and extract the program and prove it that way. This requires generally requires a type system that has a complete inference algorithm like ML type-systems and are much harder to work with and you have to set up knowing you want to do this sort of thing.
Capability systems indeed make a lot of sense for operating system level constraints and I agree this is a sensible direction and combined with type systems you can build some very powerful permission systems. But these do not solve formally verifying lots of behaviors and good capability system in my opinion (and something I worked on previous as a side project that is completely unfinished and abandoned.) need mathematical primitives and structures that lend themselves to proofs and being restricted by capabilities.
Note capabilities become a program themselves and types can become programs, so getting your types right has the same issues in the first place when talking about this level of formalization.
Formal specification presumes a priori a great deal of control over the world in general, especially the more you move away "from nature" and more towards what a human might want to instantiate themselves. Formal methods often try not to deal with things they don't "understand", or try to abstract the parts that "don't matter" away. But inevitably it changes, and the repsonse to that change is to subsume more and more into your own ontology so you understand the nuances. Or you simply control all interoperable endpoints, and so the nuances vanish away, because you're in control.
This is great when the battle is against nature. "Nature", for all its ambiguities, we generally can assume to be stable. What about with human society?
In some sense, there might not be much to formal methods if you could solve the underlying capability of getting everybody to agree on the semantics in the first place, and have no desire for change at all. But that is an absurdly strong requirement. Formal methods is constantly a race to try and find good abstractions and then breaking them.
I don't think there really is a way out of this, but I'm not that creative :/
Please check the data centric OS proposed by Stonebreaker and his team from Stanford, MIT, Google and VMware, and the pre-cursors to it namely TabulaROSA by the MIT team and also Twizzer from UC Santa Cruz [2],[3],[4].
These are excellent books by Dave McComb on the subject of data-centric software paradigm and why we need this new paradigm shift [5].
[1] Why We Need A Data-Centric OS For AI:
https://www.nextplatform.com/control/2025/05/27/why-we-need-...
[2] DBOS: A DBMS-oriented Operating System [PDF]:
https://vldb.org/pvldb/vol15/p21-skiadopoulos.pdf
[3] TabulaROSA: Tabular Operating System Architecture for Massively Parallel Heterogeneous Compute Engines:
https://dspace.mit.edu/entities/publication/69c8906b-440f-49...
[4] Twizzler: A Data-centric OS for Non-volatile Memory:
https://dl.acm.org/doi/10.1145/3454129
[5] Software Wasteland and The Data-Centric Revolution:
This is one of the real limits of formal verification. Defects or subtle inconsistencies in hardware are not that uncommon. This is mitigated to a some extent by using assertions in release builds but this has significant limitations.
* 49% : specification error - wrong thing built in the right way
* 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)
* 2% : code bugs
formal verification won't eliminate that 2%. it might get it down to 1%. there are still two enormous elephants in the room.
this is why everyone talks about it and nobody does it.
This is why experienced devs says they spent half their time trying to get concrete requirements. You don't need to code something to know that the change request is incomplete and need more details.
> * 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)
That's the reason there's a lot of books written about architecture and the necessity to push the dependencies to the edges of your code. Easy to patch stuff that way.
> * 2% : code bugs
With good tests, you can get this down quite low.
I don't dispute this, and is infact related directly to my point, it seems that people are reading my comment as formal verification is a Panacea, I was only trying to point out that are primitives and abstractions provided by operating systems as well as programming languages are one major area that stops one from writing a formal spec.
Real formal verification is very very hard.
You do seem to miss the point that I am saying many of these subtle inconsistencies can be still complex but encoded into a formal model and I was showing how the file system abstraction adds it's own complexities.
Operating systems probably would be one thing that could be a massive project to undertake but would be worth it. We already have a formally verified micro kernel sel4 that proves lots of useful features and as you point out hardware issues an important thing at this level of correctness and sel4 simply assumes certain models for this.
I don't think so. Even if you take small embedded project, there's a lot of unreliability that could creep in. You're not really sure what you got from a sensor is good or noise. Which is why you got all those error checking and ack in the protocols. You can make assumptions and try to verify your own code, but that's only if it brings enough benefits (mostly give you a clear sense of how likely something could go wrong). And that holds only for one version of the software.
You can do reliability study on hardware because it stays mostly in one configuration. But all bets are off if you're constantly modifying stuff inside.
The problem is even formalizing a file system at all. It is nearly impossible to even effectively prove something as simple as:
1. Program A creates a file, F, that only program A writes and writes some data.
2. Program B writes file G which correctly modifies untold amounts of arbitrary file system data structures.
3. Program A reads file F and sees the contents are unchanged.
If you could easily prove that for arbitrary programs that follow those very basic rules, then you would be able to formalize like 90% of file system usage.
The weaknesses and difficultys of formal methods are at a far, far lower level than people think.
The sort of model you suggested does not map every possible state of the file system to a model state structure so one could have various problems with results of the proof.
I guess the difficulty of formal methods depends on how much and what you want to prove, there is no real formal definition as to when something becomes formal methods is a spectrum and includes algo/c type type systems to CoC proofs and extracted programs.
You are doing the metaphorical equivalent of arguing how using antimatter for power is hard because we can not efficiently harness gamma rays when the harder and more immediate problem is that we do not have antimatter.
I would say it is important when ... other systems
1. Depend on the "correctness" of our system.
2. Depend on the correctness of the assumptions the other system's spec makes about its environment
Sure, but people (perhaps including you) don't understand that it's foundational.
That is, it's not enough to be correct, but if your program isn't even correct there's basically no chance it does what you intended.
While these areas were main premise of an article when it was written, I think the article really aged well into current time of mass AI/LLM deployment. It shows fundamental limitations of token based systems / symbolic reasoning that LLM espouses internally, while writing correct software. These limitations also apply to humans, however humans mental modelling, being not fully based on symbolic processing, have been historically shown capable of writing correct software systems, while AI/LLM systems have not been proven to be able to do that, and as article shows that with current token based technology it's unlikely they will ever be.
I think those domains has more stringent requirement and a more focused usage, making the classes of inout narrower. A lot of software for B2B and B2C tries to be a kitchen sink and in the result get turned into a ball of mud. Some stuff should just be separate software.
The software is always interpreted in the real world, and you can always convert the software plus the interpreter into a mathematical proof (via Curry-Howard isomorphism) that given input gives a given output. It is mathematically equivalent to running a program, up to the reliability of the interpreter and correctness of the mathematical model of the interpreter.
What might be a bit harder, to show, that a set of inputs causes a set of outputs. But that's just partial interpretation and depending on properties, in practical programs quite doable.
And frankly, existence of LLMs shows that you can quite easily prove most program properties. When LLM creates a program it translates a program description in natural language together with formal version of natural language (which it has from training) into a computer program. In other words, LLM doesn't work with the real world, but with a model of the real world. Although LLM's world model is not sound (in the sense that logical fragment of its reasoning has not been proven sound), many people are mostly happy with the results. This shows that LLM can preserve properties between the description of the program in natural language and the world model embedded in LLM (these often include implicit desirable properties), and the resulting source code to be executed. And if you're able to preserve the properties, the actual sound proofs transfer by construction, too (up to the few cases where LLM slips and reasons unsoundly, but AI labs are trying hard to reduce these cases to minimum).
This does not require proving systems complete correct, but it does involve proving many properties of these systems.
We ought to be able to build high-confidence software.
Unless you have bamboozled your customers completely, they should expect a product that you provide to be a) fit for purpose, b) fit for use, and c) secure.
We know of course that very little commercial software is (d) proven correct. Software Correctness (d) is hard, no question.
Just getting to ONE of { a, b, c } appears to be a bridge too far. But that's where professional rigour and diligence is required.
btw good article, u/turbobutton.
We are, it's just incredibly expensive.
Cheers!
Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API.
So I had to reconstruct a signal that fitted the data for the equations to work at all. But the reconstruction was no longer measured data. It was made up, and there was no single solution for fitting the data. That meant I could claim to "respect the data" while producing any result I wanted.
Indeed: here are two papers on this topic:
Jürgen Mayer; Khaled Khairy; Jonathon Howard. Drawing an elephant with four complex parameters. 2010. https://pubs.aip.org/aapt/ajp/article-abstract/78/6/648/1042... Article without paywall : https://publications.mpi-cbg.de/Mayer_2010_4314.pdf
Dian Jin; Junze Yuan. Fitting an Elephant with Four non-Zero Parameters. 2024. https://arxiv.org/abs/2407.07909v1
a fun one that immediately comes to mind is asserting something holds for reals, but not evaluating whether it holds for IEEE floats, though maybe that's not really a thing in finance due to rounding related rules anyways
The same argument goes for type safety in general: would you rather "know" how it all works all the time and make the changes without assistance (ample evidence this is generally not possible beyond toy scale) and discover later what you missed, or encode expectations into types so a significant chunk of it is "chase compiler errors"?
No location on that continuum is ideal in all cases, there's plenty of room for variety.