Why Writing Correct Software Is Hard
pron.github.io
pron.github.io
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...
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
This does not require proving systems complete correct, but it does involve proving many properties of these systems.
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.
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.
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 the 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.
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.
Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API.
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.
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!
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.
Correct with regards to a formal specification?
How do we know the specification is "correct"? By definition?
It works for me, and says:
Using lightweight formal and semi-formal methods gives likely-correct software at a very affordable cost.
A case study: https://www.osequi.com/studies/list/list.html
Now, after the LLMs made formalisation thus correctness 'cheap' I can affirm:
LLMs—with the right guardrails and tools—can safely automate the design, implementation, and verification of production-ready software. What’s left for humans is to understand the problem and steer the machine toward a solution. This is production-ready software development at the speed of thought.
If people from three different business units were looking at the same system would they all agree on what "correct" is?
I have experience with multiple companies with over $100 Million/year in revenue where different departments have different definitions of what counts as a sale. So to report sales numbers you have to figure out which department is providing the numbers and which department is the audience and recalculate the figures.
The sales team wants to count a sale as any signed commitment to purchase so they can get their bonus, the finance team might only want to count what has been paid for and the warehouse might only care about shipments. There's no amount of formal verification that can overcome these kinds of politics of a business.
For a given program and a one off proof one can prove many things or if we over approximate by assuming loops terminate we can prove many things soundly with the risk of rejecting programs that are sometimes correct (eg type systems).
This may have been a quirk of language or my interpretation though.
It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.
Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.
One small nitpick:
A 4K challenge normally refers to code that fits in 4KB, but a straightforward encoding of a 1919 state TM takes 19192(2+11) = 49894 bits, or 6237 bytes, over 6KB.
Recent AI-fueled optimizations have lowered the count to at most 215 states though, which fits comfortably in 1KB...
Sure, by Rice's theorem, no program can decide whether an arbitrary function always computes the sum of its two inputs. But that's only because we are allowing arbitrarily difficult-to-analyze implementations of the sum function. So this theorem co-exists with the fact that simple implementations of sum can be proven correct.
In this light I think the best conclusion is "to write correct software in reasonable time, we must use easy to analyze languages and program styles".
I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language
Putting limits on a scripting language should not be too hard (even without talking about any correctness proof). And I would bet that for a scripting language where the limits are in a way that "in a correct implementation, it should be highly likely that these limits are actually enforced" (i.e. the specification of the scripting language has no parts that makes you suspicious whether there exists some loophole that a malicious actor could use to overstep the limits), it should actually be possible to write a verified implementation with some effort.
But this is not what people want: for example, basically every evolution of the web standards since HTML5 by the WHATWG was about extending what is possible to do in the scripting language (JavaScript).
I might want my code to dabble in CORS, read env vars, or snoop around in my .ssh directory, but I don't want my imports to be able to do that.
OpenBSD has a (partial?) solution for that: pledge (2)
https://man.openbsd.org/OpenBSD-6.7/pledge.2
Often, a programming needs a lot of rights at the start to set things up (often even root permissions). After this has been done, it should better have irrevocable limited rights. The pledge() syscall is there to do this transition:
"Subsequent calls to pledge() can reduce the abilities further, but abilities can never be regained."
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.
A heck of a lot. Your professor clearly does not know much about astronomy.
The same can be said about computers and computer science. I don't think I fully agree with that, but it's interesting to think about.
For example if you have a whole bunch of Hydrogen the gravity its exerting on itself is negligible... Unless it's a lot of Hydrogen because eventually instead of being negligible the gravity adds up to where the Hydrogen atoms undergo nuclear fusion and that's how you get stars.
Similarly, Oceanography does have boats and a large building next to the sea, but although some of them are capable sailors, a lot of what they're interested in is theoretical and doesn't require you to even be able to smell the sea, let alone go out on it.
The reason we know anything about the composition of stars, the distance to galaxies, their relative speed etc. is because we use a telescope and study spectral lines.
Your comparison of oceanography and boats is a poor analogy. The a analog to telescopes would be sonar (and maybe seismographs?). The analog to boats would be spaceships/rockets. This makes my point.
- Computer science is about extending our understanding what can be done with computers (including what can be done efficiently). The computer scientist in this story exactly does that: he sees that the usage of the poster is a special case of a much more general pattern, and tries to understand this pattern, so that a solution that is developed for the general case can be applied to all of them, without having to develop a novel solution for every new case, which can save an insane amount of money.
- The kind of requirement analysis, and process orientation is rather untypical for computer scientists, but rather for what is called in German "Wirtschaftsinformatiker" (i.e. people who are business process analysts first and programmers second). These are people who are deep in love with such analysis paralysis, not the typical programmer or computer scientist who is often quite suspicious of such concepts.
In other words: if your toilet is clogged, you call a plumber, and not an expert in fluid dynamics.
This was in the early-ish days of OOP, when people were saying that, to design software, you were to "write a story" on how you want it to go. The nouns were objects, the modifiers, functions, and the verbs, program flow (or something like that. I never used it, as I thought it was silly).
That kind of thing was very attractive to upper managers, who dreamed of firing all the filthy engineers, and writing the code, themselves.
Sort of like now, with vibe-coding.
> plus ça change, plus c'est la même chose
I thought managers typically feel "above" writing code themselves. :-)
> I believe that Dijkstra's quote should be attributed to Mike Fellows, since it is fairly clear that Dijkstra heard it from him. Although the earliest appearance in print appears to be in our 1993 article, in my opinion Mike deserves sole attribution. He made up the part that is quoted so widely. I simply tacked on a bit at the end that nobody bothers to quote. Here it is again, correctly attributed for posterity.
Says this guy: ianparberry.com/research/cseducation/
But that's 1993, and MIT 6.001 Structure and Interpretation, 1986 has an extremely similar quote (though doesn't actually mention telescope + astronomy).
I'm writing this comment live, and I just found this! https://quoteinvestigator.com/2021/04/02/computer-science/
Variations of this has been said by many people, over a fairly long period of time. Fascinating :-).
La Palma - Gateway to the Universe (November 9, 2026)
The team journey to La Palma, where giant new telescopes and cutting-edge science are opening extraordinary new windows on our universe.
Roque de los Muchachos Observatory - https://en.wikipedia.org/wiki/Roque_de_los_Muchachos_Observa...
And an astronomer should absolutely have understanding of those, their intricacies, the optical equations involved, and how to operate them (usually with automated software, but astronomers are the ones writing that software).
Now an astrophysicist has less to do with telescopes, especially if your field is theoretical cosmology, although they still require familiarity with telescopes, practicalities, how observations are made etc. because that is the basis of their theory. So, a cosmologist vs. an astronomer might be a better analog for a computer scientist vs. a software engineer.
And I know that despite doing my own thesis in cosmology, my studies involved a lot of knowledge and teaching about telescopes, including at least one night of observations (it's pretty boring, things are very automated).
Doing a brick layer training doesn't make one a construction builder.
Disagree about what? You've certainly recognized that professional engineers have tried to usurp the term for their own devices, but that was already called out earlier. There was never a disagreement there. The word "engineer" predates societies of engineers by several hundred years or more so there is no claim that those societies came up with it, so there is nothing to disagree about there either.
> Doing a brick layer training doesn't make one a construction builder.
If someone goes to a bootcamp and then, following that, sits on the couch watching TV until their end of days then you're right that they would not be an engineer. But I have never seen anyone claim that they are something when they aren't doing it. Someone who worked at McDonalds when they were 14 years old and never again don't still call themselves a fast food worker when they are a 50 year old CEO, so I am not sure this take logically follows. It was implied that there is associated action.
The terminology of the "halting problem" is a very specific term of computer science, and it didn't age badly. This is like saying a reactor "going critical" hasn't aged well because non-physicists don't understand what "critical" means: it's not meant for them. Or about "prime numbers" because non-mathematicians don't know what "prime" means. Or what a "continuous function" is, etc, etc. You get the idea.
Modern programs are still composed of functions, and those functions are subject to the halting problem, in the sense that they get inputs and provide outputs. If they don't, they did not "compute" in precisely the sense you meant it. So let's say your videogame or whatever is waiting for input (the joystick or mouse) and you don't provide it, and because it's a turn-based game, nothing else happens. Has it "halted" in the sense we're discussing? Nope. It would be subject to halting if, once you provide input, the program cannot produce the intended result for your input (move a sprite, display "game over", start another round, play an animation, modify internal game state, etc).
In other words, Computer Science talks of "programs" but it's really any computation that takes an input and produces an output, and modern programs are made of them, so the problem applies to them.
My favourites are "normal" and "almost all". Almost All real numbers are Normal.
If you choose an answer to this question at random what is the chance you will be correct?
A) 25% B) 50% C) 0% D) 25%
Maybe I'm wrong but I believe this problem and the halting problem are versions of Gödel's incompleteness theorem. In the realm of probability theory and computing science respectably. Basically, I see it as the inability of a set of rules to reason (or be applied) to themselves.
This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming. That's why they are terrible for games and websites, domains where correctness doesn't matter as much as feeling and iteration speed. Sure, it would be nice if those programs had no bugs, but basically any means of increasing iteration speed and flexibility is worth it.
A startup or indie usually has a short runway. Saying we're going to half that so we can make sure we don't have any memory leaks is a laugh. It may cost 10s-100s of $K, or be the difference in launch / failure.
We basically would not have AI today if it weren't for loosey-goosey riddled-with-holes languages like python with all the symbolic madness they enable. The ability of researchers to write a few lines and run it without regard to memory, processor layouts, etc. was what enabled them to write these programs at all. Of course we've put lipstick on the pig with CUDA and torch "compiling" compute graphs, its actually such a beautiful disaster that most software runs on JS or python, two horrid languages that have so much work to make them just performant enough.
I have no idea how to go about it, but it would be very cool to have a system where you can take the soft clay approach, while having a compiler that can effectively tell what it can prove about the program, and what it can't, and as you figure out the right shape of the program, you tighten it up until you have the level of proof you're happy with.
> This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming.
I will say, this was my experience when starting out with Rust, but after working with it for a while and "internalizing" it, I actually find it to be quite quick to experiment with.
Management and marketing can only cope with a vague, third party description of the sheet.
Reminds me of the XKCD with the mathematicians all the way over there... Oh, hi!
Ironic that multiple levels of abstraction understanding, from mathematics to physics to hardware to software to management and marketing are all required to make a single, successful product that can touch the world. All these eyes of needles to be lined up and threaded.
It's nice to stand back in awe occasionally. Then return to complaining about hardware prices and AI slop ;)
In particular, I think its deductive proofs section is unnecessarily pessimistic. People have some idea as to why their code is correct when they write it. They're occasionally wrong (at a typical rate of single-digit bugs per 1k SLOC), but you can't often write an approximately correct program without an approximately correct proof of correctness in your mind. Yes, it's true that some proofs are intractably long, but that doesn't apply to the code we actually write. A language requiring you to write out those things you're relying on and concluding isn't much more verbose than any other programming language, and that mental scaffolding makes automated theorem proving vastly easier. You'll still fail to validate correct programs from time to time, but you solve that the same way the Rust people do -- add escape hatches and/or change your code to match the solver's limitations.
Even quite complicated externalities are similarly solvable. People talk about time and filesystems and what have you as unprovable balls of mud, and ... they're right ... but that misses the point. Precious little software handles an FS correctly. That's all the level of proof your program needs; not that you never corrupt your save state, but that if no other process mucks around with your data then you never corrupt your save state. For better software (like TigerBeetle) with stronger guarantees, well, they've already written their own proofs of correctness. All that remains is tying them to the actual implementation.
But if you have a basic understanding of computational complexity and Turing machines, plus a general knowledge of basic programming and CS, you should be able to follow the article well enough to get something out of it, I think.
How often we use full int16 for counting things? Even stuff like video frames we can easily limit size_t to fixed values like `{1920x1080, 1920x1080x3 , 1920x1080x1.5, 1080}` (representing common memory sizes for 420/RGB frames).
So instead of validating the whole infinite space of all possible states, we can carve tiny tunnels in this hypercube and significantly reduce that surface of proof.
I know that in the AI era, with code being generated in enormous quantities, formal verification is important. It is effective to some degree, but in my view, software that requires provable correctness is only a subset of all software, and I agree with the author that a kind of empiricism is the right approach. Because most of it is based on understanding a customer's "requirements." And if we consider that not all requirements can be formally proven mathematically, then in practice the line between where formal verification is used and where it isn't will become clearly drawn.
Formal specification is the work of deciding where the target is, and formal verification is the work of hitting that target with an arrow. But most of software development is the work of deciding where the target ought to be. Formal specification is like shooting an arrow at a moving target and hitting the bullseye, but figuring out where to pin that target down is software development, and honestly, most of software development spends more time pinning the target's position. Especially in the AI era, even more so.
You can't formally verify code when the code hasn't even met the spec yet! It takes a huge amount of time and effort to achieve this! Even when you think you've achieved this and your code meets the spec word-for-word, some stakeholders will still disagree based on technicalities and definitions!
How in the world are we supposed to prove that code is correct when people can't even agree on the same definition of 'correct'?! That's most of the work, really.
Also, if it takes people 1 year to complete a project in such a way that it barely just meets the spec to an acceptable standard, and only in a pure high level business sense; just barely covering all the basic exception handling scenarios; how long is it going to take to add formal verification on top of that? How many more gaps will have to be plugged, how many more assumptions will need to be enumerated, in order to make your formal proof air-tight? Then what happens if the client reads your formal proof and informs you that some of your assumptions are incorrect? What value is your proof then?