The title doesn't really match the content. TFA talks a lot about the foundations of computation and what we know about arbitrary programs, and it appeals far too much to tools like Rice's theorem to be useful in ordinary engineering contexts.
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.
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.
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...
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.
Basic problems such as change over time and interoperability are reasons why formal methods break.
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 :/
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.
> 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
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).
I don't write those sorts of programs either. There is evidence that some people do write that sort of program with varying amount of success in "draw nice". I'm sure such people could write books on what draw nice means. I would refuse such a job because I don't have the right expertise, and you probably wouldn't hire me for it even if I would accept it. However hire the right expert and you can probably get what you want even though at the start you don't even know what you really want - the other option is the expert will quickly realize is what you want is not what they can do and either tell you not to waste your money or warn you that you are going to spend a lot of money on an open ended research project that may or may not produce results.
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)
Not that vague first you need to know what the customer means by good. I was not making claims on the applicability of formal methods any way, only the point I was making about the primitives.
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.
> type systems
Indeed types systems are usually the way formal verification is done, I am not denying that. The problem I am claiming is not the tools of formal verification but the domain one has to model and capture.
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.
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.
> 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.
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.
> 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.
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.
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.
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.
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.
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
By trying to formalize a rough idea of what the correct behavior is, encountering edge cases and deciding what is correct in each case, thus refining the idea of what is correct.
The most important part of a negative claim is implicit: what reasonable assumptions might negate the claim?
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 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.
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.
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.
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).
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
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."
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).
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.
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"
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 ;)
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"
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....
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.
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.
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.
"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.
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.
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.
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).
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 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.
> 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 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.
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.
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.
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.
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.
> 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.
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.
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.
Exactly. I've worked on complex year-long projects where we've just been working non-stop, each team member generating thousands of lines per day and 1 year isn't enough to plug all the gaps in the spec with code and to cover all the exception handling cases at an MVP level.
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?
The title doesn't really match the content. TFA talks a lot about the foundations of computation and what we know about arbitrary programs, and it appeals far too much to tools like Rice's theorem to be useful in ordinary engineering contexts.
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.
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.
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...
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.
Basic problems such as change over time and interoperability are reasons why formal methods break.
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 :/
Customer request: make a software that makes drawings that look good/my style/...
Where do you start for formalizing this?
You start by defining a loss function.
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
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.
> 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
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).
I don't write those sorts of programs either. There is evidence that some people do write that sort of program with varying amount of success in "draw nice". I'm sure such people could write books on what draw nice means. I would refuse such a job because I don't have the right expertise, and you probably wouldn't hire me for it even if I would accept it. However hire the right expert and you can probably get what you want even though at the start you don't even know what you really want - the other option is the expert will quickly realize is what you want is not what they can do and either tell you not to waste your money or warn you that you are going to spend a lot of money on an open ended research project that may or may not produce results.
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)
Not that vague first you need to know what the customer means by good. I was not making claims on the applicability of formal methods any way, only the point I was making about the primitives.
Inductively, in which case data labels are the spec and having good data is still the hardest part ;-)
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.
> type systems Indeed types systems are usually the way formal verification is done, I am not denying that. The problem I am claiming is not the tools of formal verification but the domain one has to model and capture.
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.
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.
> 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.
>We ought to be able to build high-confidence software.
We are, it's just incredibly expensive.
As a witty person once said, good software is expensive to make... and so is bad software.
Cheers!
> 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.
What I've learned this year is that we should be verifying the fridges..
Or thought more carefully about putting them on any LAN directly.
We should think hard before putting anything on the internet.
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.
> 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.
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.
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.
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.
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.
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.
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."
> "With four parameters I can fit an elephant, and with five I can make him wiggle his trunk."
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
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
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?
By trying to formalize a rough idea of what the correct behavior is, encountering edge cases and deciding what is correct in each case, thus refining the idea of what is correct.
The most important part of a negative claim is implicit: what reasonable assumptions might negate the claim?
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 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.
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.
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.
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).
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
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.
> 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."
> 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).
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.
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"
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 ;)
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"
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....
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.
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.
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.
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.
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.
I think bootcamps did more of a disservice, especially when folks come out of them calling themselves "engineers".
"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.
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.
> I fully disagree
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.
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.
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).
Reminds me of the classic The Parable of the Toaster:
https://www.glaver.org/ftp/humor/toaster-fable.txt
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 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.
I'm pretty sure its a quote from Dijkstra.
It is, but maybe he had Dijkstra as a professor.
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 :-).
> as an astronomer has to do with telescopes
A heck of a lot. Your professor clearly does not know much about astronomy.
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.
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.
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.
Don't astronomers use telescopes?
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)
~ https://thetvdb.com/series/the-sky-at-night/episodes/1205884...Roque de los Muchachos Observatory - https://en.wikipedia.org/wiki/Roque_de_los_Muchachos_Observa...
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.
> 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.
> 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.
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.
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.
Exactly. I've worked on complex year-long projects where we've just been working non-stop, each team member generating thousands of lines per day and 1 year isn't enough to plug all the gaps in the spec with code and to cover all the exception handling cases at an MVP level.
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?
TLDR: programming isn't math and therefore most programs cannot be proven correct.