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.
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 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
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).
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.
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.
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 ;)
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.
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.
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.
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.
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.
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....
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.
That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...
Think about the filesystem, the big issue with formalizing a program spec that operates on a file system is simply the fact it is essentially a shared object amongst all the programs running on the system. Add to that the fact that (though this changes with modern containerization systems, namespaces, pledge what ever) a program may at any point gain access to root permissions if it makes the system call to do so providing the correct credentials it becomes very difficult formally be able to remove any possible states from the system.
All this could be different but we would radically need to redesign are systems and the way we think about the problems.
Where do you start for formalizing this?
An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write.
While these areas were main premise of an article when it was written, I think the article really aged well into current time of mass AI/LLM deployment. It shows fundamental limitations of token based systems / symbolic reasoning that LLM espouses internally, while writing correct software. These limitations also apply to humans, however humans mental modelling, being not fully based on symbolic processing, have been historically shown capable of writing correct software systems, while AI/LLM systems have not been proven to be able to do that, and as article shows that with current token based technology it's unlikely they will ever be.
I think those domains has more stringent requirement and a more focused usage, making the classes of inout narrower. A lot of software for B2B and B2C tries to be a kitchen sink and in the result get turned into a ball of mud. Some stuff should just be separate software.
This does not require proving systems complete correct, but it does involve proving many properties of these systems.
Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API.
So I had to reconstruct a signal that fitted the data for the equations to work at all. But the reconstruction was no longer measured data. It was made up, and there was no single solution for fitting the data. That meant I could claim to "respect the data" while producing any result I wanted.
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
Correct with regards to a formal specification?
How do we know the specification is "correct"? By definition?
For a given program and a one off proof one can prove many things or if we over approximate by assuming loops terminate we can prove many things soundly with the risk of rejecting programs that are sometimes correct (eg type systems).
This may have been a quirk of language or my interpretation though.
It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.
Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.
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
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 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).
Management and marketing can only cope with a vague, third party description of the sheet.
Reminds me of the XKCD with the mathematicians all the way over there... Oh, hi!
Ironic that multiple levels of abstraction understanding, from mathematics to physics to hardware to software to management and marketing are all required to make a single, successful product that can touch the world. All these eyes of needles to be lined up and threaded.
It's nice to stand back in awe occasionally. Then return to complaining about hardware prices and AI slop ;)
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
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.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.
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).
https://www.glaver.org/ftp/humor/toaster-fable.txt
- 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.
A heck of a lot. Your professor clearly does not know much about 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.
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.
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...
The terminology of the "halting problem" is a very specific term of computer science, and it didn't age badly. This is like saying a reactor "going critical" hasn't aged well because non-physicists don't understand what "critical" means: it's not meant for them. Or about "prime numbers" because non-mathematicians don't know what "prime" means. Or what a "continuous function" is, etc, etc. You get the idea.
Modern programs are still composed of functions, and those functions are subject to the halting problem, in the sense that they get inputs and provide outputs. If they don't, they did not "compute" in precisely the sense you meant it. So let's say your videogame or whatever is waiting for input (the joystick or mouse) and you don't provide it, and because it's a turn-based game, nothing else happens. Has it "halted" in the sense we're discussing? Nope. It would be subject to halting if, once you provide input, the program cannot produce the intended result for your input (move a sprite, display "game over", start another round, play an animation, modify internal game state, etc).
In other words, Computer Science talks of "programs" but it's really any computation that takes an input and produces an output, and modern programs are made of them, so the problem applies to them.
My favourites are "normal" and "almost all". Almost All real numbers are Normal.