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...
Why Writing Correct Software Is Hard (pron.github.io)
170 pointsby AriFordsham4 hours ago68 comments
turbobutton 3 hours ago
I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Any software that's processing inputs and provides complex workflows to humans has to necessarily deal with the endless vagaries of reality.
turbobutton 2 hours ago
Having been downvoted, I like to clarify that this comes from the experience working in finance with developers with a strong academic background that emphasized on the necessity of formal proof to a point where complexity made actual progress nearly impossible- while simultaneously basing the proof repeatedly on assumptions that did not uphold in practice.
i_am_a_peasant 2 hours ago
Nah I don't disagree with you. Thing is even if you formally prove that for every input you produce a valid output. In safety certified software, there's the problem that if that input comes from a sensor, a sensor is an inherently probabilistic thing, and it may be that you will have false positives. The best you can do is build a safety case that even if you get false positives you end up in a safe state, but you can't guarantee that they won't ever increase operational costs.
bajard 2 hours ago
I once had a sensor that rounded the data, so the output unwittingly fitted into a grid. The equations that had to be used on that data gave infinite results because the grid sometimes rounded slopes into vertical lines.
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.
i_am_a_peasant an hour ago
Reminds me of that von Neumann quote "With four parameters I can fit an elephant, and with five I can make him wiggle his trunk."
perching_aix 2 hours ago
what were some categories of such assumptions, can you name some examples?
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
ekidd 2 hours ago
There is a wide range of software that exists in a "adversarial" environment, including anything facing a network or processing outside data. At a minimum, this software should should not allow an attacker to execute code of their choice on a system handling private data.
This does not require proving systems complete correct, but it does involve proving many properties of these systems.
darkwi11ow 2 hours ago
I agree with you that for most software, verification was historically less of the requirement, however some software always needed to have abstract, mathematical correctness -- think military, medical, industrial automation.
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.
skydhash 2 hours ago
> however some software always needed to have abstract, mathematical correctness -- think military, medical, industrial automation.
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.
xpct 2 hours ago
What I've learned this year is that we should be verifying the fridges..
kodoman 2 hours ago
Or thought more carefully about putting them on any LAN directly.
tonyedgecombe an hour ago
We should think hard before putting anything on the internet.
kodoman 2 hours ago
For me it seems more like modern software has built away from using formal mathematical models in the first place, not the necessarily the problem people want to solve have to have such a fuzzy definition of domain, but that the primitives of operating systems and software development have gone in the other direction.
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.
jcelerier an hour ago
Customer request: make a software that makes drawings that look good/my style/...
Where do you start for formalizing this?
yababa_y an hour ago
for example here was how some design rules got formalized into a checker during a video editing session of several hours: https://github.com/emberian/vidbox/blob/dev/render/drc.py
kodoman an hour ago
I mean would you take that spec as something you could deliver? This is not a real problem spec and is incredibly vague, but the first question would be around building a formal model for the drawing part of the application (and is the main aspect of the program) that might be easier then it first seems. There are various ways you could model the draw window depending on if it's a rasterizing program or a vector program either way not challenging, then formalize the operations of the program (various effects will necessary be well defined mathematical functions in the first place) and then prove what ever you feel you have to prove about the system. This is not to say it is easy or especially in this case you should even do it and my point was more about the system aspect of things or things that one would want to be able to reason about.
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.
jcelerier 35 minutes ago
> I mean would you take that spec as something you could deliver?
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
kodoman 19 minutes ago
I don't write these sort of programs but my thinking is that 'draw nice' is vague and I would not know what that means and indeed that is a fuzzy spec I would have only thought you needed more clarification on what good or nice here means and it sounds like what you do is actually work out most of what the program has to do and really they have asked you to make them a drawing program with them giving you input along the way.
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).
bluGill 18 minutes ago
That is very common for something given in the industry. It is our job as programmers to first figure out what the customer really wants, and then create enough of the requirements/spec to deliver it. That is one of the reasons for Agile vs Waterfall processes: nobody really knows what they want in the first place so you deliver something that you think is close and work with them to come up with something acceptable (acceptable covers both it does what they want, and also the cost to make it better). Any formal spec needs to be adjustable as we figure out requirements.
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)
fultonn 24 minutes ago
Inductively, in which case data labels are the spec and having good data is still the hardest part ;-)
hackingonempty 23 minutes ago
You start by defining a loss function.
ModernMech 29 minutes ago
I don't think it has to be radically different... type systems are one example of formal models which languages have been moving towards recently. Especially with how they synergize with AI. Mainstream type systems are limited, but AI can use esoteric type systems with stronger guarantees, like capability permissions systems, which solve some of the issues you're highlighting.
fsloth 2 hours ago
You can combine both sometimes in application logic.
Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API.
tialaramex 40 minutes ago
> I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world.
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.
heresie-dabord 21 minutes ago
> 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...
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.
godd2 13 minutes ago
>We ought to be able to build high-confidence software.
We are, it's just incredibly expensive.
mpweiher an hour ago
I think you have to first figure out what "correct" even is.
Correct with regards to a formal specification?
How do we know the specification is "correct"? By definition?
johnbender an hour ago
As best I can tell the article wrongly conflates Rices Theorem with the idea that one can’t prove something about the small program generated by Yedidiya and Aaronson but that’s not what Rices Theorem tells us. Instead it tells us that we can’t come up with a general method to determine yes or no correctly for all programs whether a program reaches a given point.
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.
kodoman 3 hours ago
I was always interested in formal verification but have only written toy proofs and derived programs.
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.
program_whiz 23 minutes ago
Formal verification is like working with stone. If you already know the form you want, then doing so provides a rigid, long-lasting strong structure. If you're just trying things out, then its better to sketch or work with soft clay to try the forms and see what works.
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.
myrmidon an hour ago
I found it interesting how the lower bound for the BB(6) champion (2-symbol 6-state busy beaver) dates the article: It gives >10^36534, but the current champion (mxdys 2025) is >10↑↑10↑↑10↑↑8 (10↑↑8 is a power tower 10^10^10^10... eight high, and the expression is resolved right to left, so 10↑↑10↑↑8 is already completely unimaginably large).
bluGill 2 hours ago
The real question is: for a typical program we prove it - even though we know there are programs we can't prove?
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
aleph_minus_one 2 hours ago
> 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).
mrkeen 2 hours ago
It's certainly not the whole story, but I haven't seen a better vehicle for trustworthy code than pure functions.
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.
aleph_minus_one an hour ago
>
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."
BLKNSLVR 2 hours ago
Only developers see software in it's full resolution. The rest of us see an abstraction; the sheet lying over the top of a device that will never actually be unveiled due to its grotesque appearance. The public can barely even handle the aesthetics of the sheet.
Management and marketing can only cope with a vague, third party description of the sheet.
dist-epoch an hour ago
Hardware engineers say the same thing "only we see a computer in it's full resolution, software engineers see just an abstraction which hides the grotesque reality"
BLKNSLVR an hour ago
Can't disagree with that.
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 ;)
stackedinserter 3 minutes ago
Ok, my 1/100 of Goldbach IQ brain disagrees. Real life computer programs rarely operate in infinite precision numbers. We write business logic, API's and calculate salaries.
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.
lionkor an hour ago
I adore that it has become normalized in vibe-coding circles to go "actually, maybe correctness doesn't exist! as long as it runs on my machine it's fine"
dingdongditchme an hour ago
One of my biggest fear in AI boom is the loss of reliability in computing. It is such a miracle how many operations a CPU can execute correctly in a millisecond. Now we are starting the era where computers make mistakes and we have a black block neural network which no one can diagnose in the same way we could traditional software. No debuggers, no opcode, just prompts....
cowboylowrez an hour ago
yeah toss alignment mistakes into that bubbling caldron and who knows what sort of little timebombs will be spreading about in the worlds software, its like "trusting trust" level shit except we know these robots like to break into things.
bigfishrunning 37 minutes ago
The problem is reliability in computing has been a problem long before AI -- remember Windows 95? Honestly our society-scale apathy is coming home to roost at this point.
samiv 3 hours ago
Maybe it's just me but the terminology used in "halting problem" didn't age well.
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
xnorswap 3 hours ago
A lot of the language of computer science doesn't translate well to software development.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.
w4der 2 hours ago
I had a professor once say that a computer scientist has as much to do with computers as an astronomer has to do with telescopes.
zombot 2 hours ago
Don't astronomers use telescopes?
frutiger 2 hours ago
> as an astronomer has to do with telescopes
A heck of a lot. Your professor clearly does not know much about astronomy.
roelschroeven 2 hours ago
I think the point is that yes, of course telescopes are important to astronomers, but they're not the essence, they're not what the study is about. They are the tools of the study, not the object of the study.
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.
tialaramex an hour ago
It varies. I used to work for a Physics and Astronomy department, yes, some of them are interested in telescopes, of various sorts, and indeed that's the department running the scheme where lay people can look at interesting stuff in the sky using a mid-size optical telescope. But, there's a lot of deep physics, that's why it's a physics department. At scale some of the physical properties from everyday life we usually don't notice stop being negligible and because we're small that scale is called astronomy.
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.
frutiger 26 minutes ago
Perfect - your background means I can speak a language you will understand.
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.
ChrisMarshallNY 2 hours ago
Reminds me of the classic The Parable of the Toaster:
aleph_minus_one 2 hours ago
I think this article is highly unfair to computer scientists:
- 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.
the_af an hour ago
The joke also conflates computer scientists with an architecture astronaut / software engineer (whatever that means, let's say a practitioner who works writing software for a living), which alas! is all too common.
roelschroeven 2 hours ago
I'm pretty sure its a quote from Dijkstra.
torcete an hour ago
It is, but maybe he had Dijkstra as a professor.
my-next-account 37 minutes ago
It's not clear who said it first.
> 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 :-).
defrost 2 hours ago
Tell him he knows little about astronomy and invite him to watch the latest episode of The Sky at Night - a bunch of astronomers gush over a diverse set of telescopes ...
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...
Aerolfos 2 hours ago
Astronomers should have quite a lot to do with telescopes. You might say a modern astronomer has little to do with telescopes as imagined by a layperson, that is some glass lenses in a tube on a tripod, but they're still called "telescopes" even when it's a complex arrangement of mirrors housed inside an observatory (or on a satellite, as is the case of the James-Webb telescope).
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).
rjbwork 2 hours ago
And yet, the amount of slop I've seen produced to solve a problem that is trivially reduced to e.g. graph traversal on more than one occasion is astounding. I tend to think it's got more advantages than disadvantages and we should be gatekeeping harder.
pjmlp 2 hours ago
I think bootcamps did more of a disservice, especially when folks come out of them calling themselves "engineers".
win311fwg 27 minutes ago
"Engineer" is the word in the dictionary most fitting for it. The actual disservice was PEs, like the story of physicians deciding to call themselves doctors, trying to latch on to "engineer" to give their group credibility and muddying the waters. They could have just as easily given themselves a unique name to represent the unique group they want to be, but it is hard to market that. It is always easier to try and usurp a term the people already buy into.
pjmlp 6 minutes ago
I fully disagree, unless they took part into an university degree certified by the Engineers order of the respective country, with the only piece missing being the professional board exam.
Doing a brick layer training doesn't make one a construction builder.
the_af 2 hours ago
> A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
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.
tialaramex an hour ago
> Or about "prime numbers" because non-mathematicians don't know what "prime" means
My favourites are "normal" and "almost all". Almost All real numbers are Normal.
torcete an hour ago
Talking about the halting problem. Sometimes I come across a meme that asks this question:
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.
jdw64 39 minutes ago
Sometimes I wonder whether Silicon Valley programmers take this kind of difficult programming as a given. I tend to think in terms of simple programs, and while formal verification isn't bad, I question whether that's really software development.
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.
hn_submit an hour ago
TLDR: programming isn't math and therefore most programs cannot be proven correct.