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.
A challenge in high-reliability software is that the systems they are running on top of have few reliable properties. Even if you formally verify some code, you have to write vastly more code to deal with the possibility that the invariants suddenly change at runtime due to an idiosyncratic failure of the environment where that formally verified code runs.
This is one of the real limits of formal verification. Defects or subtle inconsistencies in hardware are not that uncommon. This is mitigated to a some extent by using assertions in release builds but this has significant limitations.
> A challenge in high-reliability software is that the systems they are running on top of have few reliable properties.
I don't dispute this, and is infact related directly to my point, it seems that people are reading my comment as formal verification is a Panacea, I was only trying to point out that are primitives and abstractions provided by operating systems as well as programming languages are one major area that stops one from writing a formal spec.
Real formal verification is very very hard.
You do seem to miss the point that I am saying many of these subtle inconsistencies can be still complex but encoded into a formal model and I was showing how the file system abstraction adds it's own complexities.
Operating systems probably would be one thing that could be a massive project to undertake but would be worth it. We already have a formally verified micro kernel sel4 that proves lots of useful features and as you point out hardware issues an important thing at this level of correctness and sel4 simply assumes certain models for this.
> Operating systems probably would be one thing that could be a massive project to undertake but would be worth it
I don't think so. Even if you take small embedded project, there's a lot of unreliability that could creep in. You're not really sure what you got from a sensor is good or noise. Which is why you got all those error checking and ack in the protocols. You can make assumptions and try to verify your own code, but that's only if it brings enough benefits (mostly give you a clear sense of how likely something could go wrong). And that holds only for one version of the software.
You can do reliability study on hardware because it stays mostly in one configuration. But all bets are off if you're constantly modifying stuff inside.
> * 49% : specification error - wrong thing built in the right way
This is why experienced devs says they spent half their time trying to get concrete requirements. You don't need to code something to know that the change request is incomplete and need more details.
> * 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)
That's the reason there's a lot of books written about architecture and the necessity to push the dependencies to the edges of your code. Easy to patch stuff that way.
I think data centric system and data centric OS is the way to go, and we should move away from file centric system and filesystem oriented OS, even more so now with AI and agentic systems are on the rise [1].
Please check the data centric OS proposed by Stonebreaker and his team from Stanford, MIT, Google and VMware, and the pre-cursors to it namely TabulaROSA by the MIT team and also Twizzer from UC Santa Cruz [2],[3],[4].
These are excellent books by Dave McComb on the subject of data-centric software paradigm and why we need this new paradigm shift [5].
There is also my very much related open source product that takes a practical approach, and is inspired by this research. Kind of a modern equivalent for Transaction Processing monitors that mainframes use, based on transactional, hierarchical state machines. It has built-in verification system. Not tested under production use yet.
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 :/
That is not the hard part at all of formalizing a program spec on a file system. You just conditionalize your proof based on sane/desired usage of the file system.
The problem is even formalizing a file system at all. It is nearly impossible to even effectively prove something as simple as:
1. Program A creates a file, F, that only program A writes and writes some data.
2. Program B writes file G which correctly modifies untold amounts of arbitrary file system data structures.
3. Program A reads file F and sees the contents are unchanged.
If you could easily prove that for arbitrary programs that follow those very basic rules, then you would be able to formalize like 90% of file system usage.
The weaknesses and difficultys of formal methods are at a far, far lower level than people think.
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
The contract may be that, but then as part of that contract you work together with the client, using your experience and foresight to actually create a more detailed "spec". That is still not completely formalized, but your developers/colleagues using their experience in other projects can "draw the rest of the owl" from that semi-vague spec -- and the final delivered software is the spec itself in a way.
It's absolutely not impossible to simply add one more layer in-between the developers "drawing the rest" and delivery. They just not formalize it as software in one go, but "in two".
> 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
I think that's fine though. The exact fuzzy thing the customer wants is typically still built on top of a ton of stuff that can be verified. I'm not sure it needs to be either-or. You formalize what you can, and do your best with what you can't. Ideally (if we could find a way to make formalized software cheaper/easier to build) it would reduce time wasted on the stuff that can be formalized, and allow spending more time on the stuff that can't be.
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.
Additionally a lot of formally verified programs are done via constructive proofs where you build up the correct program from primitives and extract the program and prove it that way. This requires generally requires a type system that has a complete inference algorithm like ML type-systems and are much harder to work with and you have to set up knowing you want to do this sort of thing.
Capability systems indeed make a lot of sense for operating system level constraints and I agree this is a sensible direction and combined with type systems you can build some very powerful permission systems. But these do not solve formally verifying lots of behaviors and good capability system in my opinion (and something I worked on previous as a side project that is completely unfinished and abandoned.) need mathematical primitives and structures that lend themselves to proofs and being restricted by capabilities.
Note capabilities become a program themselves and types can become programs, so getting your types right has the same issues in the first place when talking about this level of formalization.
I don't think there is a hard dichotomy (and I also think the original article is mostly wrong).
The software is always interpreted in the real world, and you can always convert the software plus the interpreter into a mathematical proof (via Curry-Howard isomorphism) that given input gives a given output. It is mathematically equivalent to running a program, up to the reliability of the interpreter and correctness of the mathematical model of the interpreter.
What might be a bit harder, to show, that a set of inputs causes a set of outputs. But that's just partial interpretation and depending on properties, in practical programs quite doable.
And frankly, existence of LLMs shows that you can quite easily prove most program properties. When LLM creates a program it translates a program description in natural language together with formal version of natural language (which it has from training) into a computer program. In other words, LLM doesn't work with the real world, but with a model of the real world. Although LLM's world model is not sound (in the sense that logical fragment of its reasoning has not been proven sound), many people are mostly happy with the results. This shows that LLM can preserve properties between the description of the program in natural language and the world model embedded in LLM (these often include implicit desirable properties), and the resulting source code to be executed. And if you're able to preserve the properties, the actual sound proofs transfer by construction, too (up to the few cases where LLM slips and reasons unsoundly, but AI labs are trying hard to reduce these cases to minimum).
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.
> 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.
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.
Given that information can be encoded in a string of digits of infinite length, there is no limit to how precisely the elephant can be drawn. Any image file is a string of bits, a single parameter.
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
One of the arguments for formalizing it anyway is that when you inevitably make changes due to the real world, you can see exactly what else might need to change.
The same argument goes for type safety in general: would you rather "know" how it all works all the time and make the changes without assistance (ample evidence this is generally not possible beyond toy scale) and discover later what you missed, or encode expectations into types so a significant chunk of it is "chase compiler errors"?
No location on that continuum is ideal in all cases, there's plenty of room for variety.
I heard/read that the mRNA vaccine (component?) is programable. If correct and since it's hard to write a correct program the first time, then something that is inside you and inside you could be disastrous.
Right, and this also assumes "correct" isn't a moving target. Many business processes evolve over time so what was once invariant is now variable and assumptions that were always true (or false) are now occasionally not.
If people from three different business units were looking at the same system would they all agree on what "correct" is?
I have experience with multiple companies with over $100 Million/year in revenue where different departments have different definitions of what counts as a sale. So to report sales numbers you have to figure out which department is providing the numbers and which department is the audience and recalculate the figures.
The sales team wants to count a sale as any signed commitment to purchase so they can get their bonus, the finance team might only want to count what has been paid for and the warehouse might only care about shipments. There's no amount of formal verification that can overcome these kinds of politics of a business.
Now, after the LLMs made formalisation thus correctness 'cheap' I can affirm:
LLMs—with the right guardrails and tools—can safely automate the design, implementation, and verification of production-ready software. What’s left for humans is to understand the problem and steer the machine toward a solution. This is production-ready software development at the speed of thought.
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.
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.
Yes, moreover - nobody in practice creates programs that are close to be undecidable, just like no engineer uses nonmeasurable functions, they just assume everything is nicely integrable. (It might be close to true for things like cryptographic functions or pseudorandom generators, but even about these we can usually prove the things we need to know.)
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.
> a Turing machine with 1919 control states which cannot be proven to terminate (i.e., it is “independent of ZFC”). This machine is so small that it comfortably fits in a 4K challenge
One small nitpick:
A 4K challenge normally refers to code that fits in 4KB, but a straightforward encoding of a 1919 state TM takes 19192(2+11) = 49894 bits, or 6237 bytes, over 6KB.
Recent AI-fueled optimizations have lowered the count to at most 215 states though, which fits comfortably in 1KB...
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".
As dev tools are leaky language abstraction they can never be complete and thus no software crafted by current methods will ever be 100% correct; loopholes in semantics will always exist as the semantics are human bird song that cannot account for all possible states.
Humans enjoy inventing language, metaphor, to fill perceived gaps in irrational physical reality we can never resolve. To pretend we are more than meets the eye.
Entropy keeps creating need to replace, to refill through erosion of physical state.
Good luck engineering around gravity, electromagnetism, and nuclear forces across the fabric of space time chipping away at all human endeavors.
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
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).
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."
"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.
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.
Well, check out the post date. That's the first recorded instance of that story, and it has undergone metamorphosis, since. People substitute job titles. The common theme is that the first is practice, and the second, theory.
This was in the early-ish days of OOP, when people were saying that, to design software, you were to "write a story" on how you want it to go. The nouns were objects, the modifiers, functions, and the verbs, program flow (or something like that. I never used it, as I thought it was silly).
That kind of thing was very attractive to upper managers, who dreamed of firing all the filthy engineers, and writing the code, themselves.
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.
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 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.
Using telescopes doesn't make them professional telescope makers. You can be a perfectly good astronomer just by using telescopes built and maintained by other people, and you can be a perfectly good telescope manufacturer without publishing peer-reviewed astronomy papers.
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.
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 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 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).
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 ;)
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.
> 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.
I have no idea how to go about it, but it would be very cool to have a system where you can take the soft clay approach, while having a compiler that can effectively tell what it can prove about the program, and what it can't, and as you figure out the right shape of the program, you tighten it up until you have the level of proof you're happy with.
> This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming.
I will say, this was my experience when starting out with Rust, but after working with it for a while and "internalizing" it, I actually find it to be quite quick to experiment with.
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....
Have we ever had that? The ssh-hole, the php issues, and a litany of CVEs that recently surfaced are almost all originate from bugs that predate vibe coding.
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.
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.
Even quite complicated externalities are similarly solvable. People talk about time and filesystems and what have you as unprovable balls of mud, and ... they're right ... but that misses the point. Precious little software handles an FS correctly. That's all the level of proof your program needs; not that you never corrupt your save state, but that if no other process mucks around with your data then you never corrupt your save state. For better software (like TigerBeetle) with stronger guarantees, well, they've already written their own proofs of correctness. All that remains is tying them to the actual implementation.
As mentioned in the article, traditionally only a small subset of programs are such critical part of a system that there's a need to prove their correctness. Think embedded software for things in airplanes, space rockets, certain medical devices, cryptography, etc.
But those types of programs do tend to have well-defined specifications to begin with.
Sorta depends on what type of software you're writing, and if you're interested in the topic.
I would think most programmers should be able to vaguely grasp the gist of the article. But unless you’ve studied a non-trivial amount theoretical computer science, a lot of the terminology will be unfamiliar. And if your math skills aren’t sharp, you might struggle to follow the proof sketches.
But if you have a basic understanding of computational complexity and Turing machines, plus a general knowledge of basic programming and CS, you should be able to follow the article well enough to get something out of it, I think.
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?
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.
This is one of the real limits of formal verification. Defects or subtle inconsistencies in hardware are not that uncommon. This is mitigated to a some extent by using assertions in release builds but this has significant limitations.
I don't dispute this, and is infact related directly to my point, it seems that people are reading my comment as formal verification is a Panacea, I was only trying to point out that are primitives and abstractions provided by operating systems as well as programming languages are one major area that stops one from writing a formal spec.
Real formal verification is very very hard.
You do seem to miss the point that I am saying many of these subtle inconsistencies can be still complex but encoded into a formal model and I was showing how the file system abstraction adds it's own complexities.
Operating systems probably would be one thing that could be a massive project to undertake but would be worth it. We already have a formally verified micro kernel sel4 that proves lots of useful features and as you point out hardware issues an important thing at this level of correctness and sel4 simply assumes certain models for this.
I don't think so. Even if you take small embedded project, there's a lot of unreliability that could creep in. You're not really sure what you got from a sensor is good or noise. Which is why you got all those error checking and ack in the protocols. You can make assumptions and try to verify your own code, but that's only if it brings enough benefits (mostly give you a clear sense of how likely something could go wrong). And that holds only for one version of the software.
You can do reliability study on hardware because it stays mostly in one configuration. But all bets are off if you're constantly modifying stuff inside.
* 49% : specification error - wrong thing built in the right way
* 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)
* 2% : code bugs
formal verification won't eliminate that 2%. it might get it down to 1%. there are still two enormous elephants in the room.
this is why everyone talks about it and nobody does it.
This is why experienced devs says they spent half their time trying to get concrete requirements. You don't need to code something to know that the change request is incomplete and need more details.
> * 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)
That's the reason there's a lot of books written about architecture and the necessity to push the dependencies to the edges of your code. Easy to patch stuff that way.
> * 2% : code bugs
With good tests, you can get this down quite low.
Please check the data centric OS proposed by Stonebreaker and his team from Stanford, MIT, Google and VMware, and the pre-cursors to it namely TabulaROSA by the MIT team and also Twizzer from UC Santa Cruz [2],[3],[4].
These are excellent books by Dave McComb on the subject of data-centric software paradigm and why we need this new paradigm shift [5].
[1] Why We Need A Data-Centric OS For AI:
https://www.nextplatform.com/control/2025/05/27/why-we-need-...
[2] DBOS: A DBMS-oriented Operating System [PDF]:
https://vldb.org/pvldb/vol15/p21-skiadopoulos.pdf
[3] TabulaROSA: Tabular Operating System Architecture for Massively Parallel Heterogeneous Compute Engines:
https://dspace.mit.edu/entities/publication/69c8906b-440f-49...
[4] Twizzler: A Data-centric OS for Non-volatile Memory:
https://dl.acm.org/doi/10.1145/3454129
[5] Software Wasteland and The Data-Centric Revolution:
https://technicspub.com/software_wasteland/
https://voucha.net
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 :/
The problem is even formalizing a file system at all. It is nearly impossible to even effectively prove something as simple as:
1. Program A creates a file, F, that only program A writes and writes some data.
2. Program B writes file G which correctly modifies untold amounts of arbitrary file system data structures.
3. Program A reads file F and sees the contents are unchanged.
If you could easily prove that for arbitrary programs that follow those very basic rules, then you would be able to formalize like 90% of file system usage.
The weaknesses and difficultys of formal methods are at a far, far lower level than people think.
Where do you start for formalizing this?
An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write.
Yes, that's the kind of contract we take on regularly. My point is that the exact thing the customer wants/needs is the one part that can't be formalized meaningfully - it's good when we show them something and they tell us is good. Everything else doesn't matter - could be the worst UI, maybe you have to reboot the computer once before starting it and once after exiting it, maybe it leaks enough memory that you have to reboot every day anyways - what matters for them to pay you is "do they like the drawing quality" and really nothing else
It's absolutely not impossible to simply add one more layer in-between the developers "drawing the rest" and delivery. They just not formalize it as software in one go, but "in two".
I think that's fine though. The exact fuzzy thing the customer wants is typically still built on top of a ton of stuff that can be verified. I'm not sure it needs to be either-or. You formalize what you can, and do your best with what you can't. Ideally (if we could find a way to make formalized software cheaper/easier to build) it would reduce time wasted on the stuff that can be formalized, and allow spending more time on the stuff that can't be.
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).
OTOH, we can probably call a much less formal spec good enough. Just that it doesn't write past the end of buffers would be very helpful. We can also throw a bounds in - if we can't prove it in X iterations then call it false (expect to adjust X to very large)
What I was trying to show is the nightmare of modeling accurately and in a way that matters lots of operating system primitives and further reasoning about when the assumptions have been violated by the program set up.
Indeed this does not effect the stuff outside the interaction of the program with the operating system and my point when it came to modern programming primitives is that not all data structures or methods of programming lend themselves to being able to write formal proofs about them.
You might be able to have a type BigInterfaceTypeThatDoesLotsOfThings<a> but this might be impossible to formalize in any meaningful way and AI is not the panacea and this stuff is not easy and require hard thinking.
Additionally a lot of formally verified programs are done via constructive proofs where you build up the correct program from primitives and extract the program and prove it that way. This requires generally requires a type system that has a complete inference algorithm like ML type-systems and are much harder to work with and you have to set up knowing you want to do this sort of thing.
Capability systems indeed make a lot of sense for operating system level constraints and I agree this is a sensible direction and combined with type systems you can build some very powerful permission systems. But these do not solve formally verifying lots of behaviors and good capability system in my opinion (and something I worked on previous as a side project that is completely unfinished and abandoned.) need mathematical primitives and structures that lend themselves to proofs and being restricted by capabilities.
Note capabilities become a program themselves and types can become programs, so getting your types right has the same issues in the first place when talking about this level of formalization.
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.
The software is always interpreted in the real world, and you can always convert the software plus the interpreter into a mathematical proof (via Curry-Howard isomorphism) that given input gives a given output. It is mathematically equivalent to running a program, up to the reliability of the interpreter and correctness of the mathematical model of the interpreter.
What might be a bit harder, to show, that a set of inputs causes a set of outputs. But that's just partial interpretation and depending on properties, in practical programs quite doable.
And frankly, existence of LLMs shows that you can quite easily prove most program properties. When LLM creates a program it translates a program description in natural language together with formal version of natural language (which it has from training) into a computer program. In other words, LLM doesn't work with the real world, but with a model of the real world. Although LLM's world model is not sound (in the sense that logical fragment of its reasoning has not been proven sound), many people are mostly happy with the results. This shows that LLM can preserve properties between the description of the program in natural language and the world model embedded in LLM (these often include implicit desirable properties), and the resulting source code to be executed. And if you're able to preserve the properties, the actual sound proofs transfer by construction, too (up to the few cases where LLM slips and reasons unsoundly, but AI labs are trying hard to reduce these cases to minimum).
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.
We ought to be able to build high-confidence software.
Unless you have bamboozled your customers completely, they should expect a product that you provide to be a) fit for purpose, b) fit for use, and c) secure.
We know of course that very little commercial software is (d) proven correct. Software Correctness (d) is hard, no question.
Just getting to ONE of { a, b, c } appears to be a bridge too far. But that's where professional rigour and diligence is required.
btw good article, u/turbobutton.
We are, it's just incredibly expensive.
Cheers!
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.
Indeed: here are two papers on this topic:
Jürgen Mayer; Khaled Khairy; Jonathon Howard. Drawing an elephant with four complex parameters. 2010. https://pubs.aip.org/aapt/ajp/article-abstract/78/6/648/1042... Article without paywall : https://publications.mpi-cbg.de/Mayer_2010_4314.pdf
Dian Jin; Junze Yuan. Fitting an Elephant with Four non-Zero Parameters. 2024. https://arxiv.org/abs/2407.07909v1
a fun one that immediately comes to mind is asserting something holds for reals, but not evaluating whether it holds for IEEE floats, though maybe that's not really a thing in finance due to rounding related rules anyways
The same argument goes for type safety in general: would you rather "know" how it all works all the time and make the changes without assistance (ample evidence this is generally not possible beyond toy scale) and discover later what you missed, or encode expectations into types so a significant chunk of it is "chase compiler errors"?
No location on that continuum is ideal in all cases, there's plenty of room for variety.
Correct with regards to a formal specification?
How do we know the specification is "correct"? By definition?
If people from three different business units were looking at the same system would they all agree on what "correct" is?
I have experience with multiple companies with over $100 Million/year in revenue where different departments have different definitions of what counts as a sale. So to report sales numbers you have to figure out which department is providing the numbers and which department is the audience and recalculate the figures.
The sales team wants to count a sale as any signed commitment to purchase so they can get their bonus, the finance team might only want to count what has been paid for and the warehouse might only care about shipments. There's no amount of formal verification that can overcome these kinds of politics of a business.
It works for me, and says:
Using lightweight formal and semi-formal methods gives likely-correct software at a very affordable cost.
A case study: https://www.osequi.com/studies/list/list.html
Now, after the LLMs made formalisation thus correctness 'cheap' I can affirm:
LLMs—with the right guardrails and tools—can safely automate the design, implementation, and verification of production-ready software. What’s left for humans is to understand the problem and steer the machine toward a solution. This is production-ready software development at the speed of thought.
For a given program and a one off proof one can prove many things or if we over approximate by assuming loops terminate we can prove many things soundly with the risk of rejecting programs that are sometimes correct (eg type systems).
This may have been a quirk of language or my interpretation though.
It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.
Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.
One small nitpick:
A 4K challenge normally refers to code that fits in 4KB, but a straightforward encoding of a 1919 state TM takes 19192(2+11) = 49894 bits, or 6237 bytes, over 6KB.
Recent AI-fueled optimizations have lowered the count to at most 215 states though, which fits comfortably in 1KB...
Sure, by Rice's theorem, no program can decide whether an arbitrary function always computes the sum of its two inputs. But that's only because we are allowing arbitrarily difficult-to-analyze implementations of the sum function. So this theorem co-exists with the fact that simple implementations of sum can be proven correct.
In this light I think the best conclusion is "to write correct software in reasonable time, we must use easy to analyze languages and program styles".
Humans enjoy inventing language, metaphor, to fill perceived gaps in irrational physical reality we can never resolve. To pretend we are more than meets the eye.
Entropy keeps creating need to replace, to refill through erosion of physical state.
Good luck engineering around gravity, electromagnetism, and nuclear forces across the fabric of space time chipping away at all human endeavors.
I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language
Putting limits on a scripting language should not be too hard (even without talking about any correctness proof). And I would bet that for a scripting language where the limits are in a way that "in a correct implementation, it should be highly likely that these limits are actually enforced" (i.e. the specification of the scripting language has no parts that makes you suspicious whether there exists some loophole that a malicious actor could use to overstep the limits), it should actually be possible to write a verified implementation with some effort.
But this is not what people want: for example, basically every evolution of the web standards since HTML5 by the WHATWG was about extending what is possible to do in the scripting language (JavaScript).
I might want my code to dabble in CORS, read env vars, or snoop around in my .ssh directory, but I don't want my imports to be able to do that.
OpenBSD has a (partial?) solution for that: pledge (2)
https://man.openbsd.org/OpenBSD-6.7/pledge.2
Often, a programming needs a lot of rights at the start to set things up (often even root permissions). After this has been done, it should better have irrevocable limited rights. The pledge() syscall is there to do this transition:
"Subsequent calls to pledge() can reduce the abilities further, but abilities can never be regained."
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.
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.
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.
This was in the early-ish days of OOP, when people were saying that, to design software, you were to "write a story" on how you want it to go. The nouns were objects, the modifiers, functions, and the verbs, program flow (or something like that. I never used it, as I thought it was silly).
That kind of thing was very attractive to upper managers, who dreamed of firing all the filthy engineers, and writing the code, themselves.
Sort of like now, with vibe-coding.
> plus ça change, plus c'est la même chose
I thought managers typically feel "above" writing code themselves. :-)
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 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 :-).
A heck of a lot. Your professor clearly does not know much about astronomy.
The same can be said about computers and computer science. I don't think I fully agree with that, but it's interesting to think about.
For example if you have a whole bunch of Hydrogen the gravity its exerting on itself is negligible... Unless it's a lot of Hydrogen because eventually instead of being negligible the gravity adds up to where the Hydrogen atoms undergo nuclear fusion and that's how you get stars.
Similarly, Oceanography does have boats and a large building next to the sea, but although some of them are capable sailors, a lot of what they're interested in is theoretical and doesn't require you to even be able to smell the sea, let alone go out on it.
The reason we know anything about the composition of stars, the distance to galaxies, their relative speed etc. is because we use a telescope and study spectral lines.
Your comparison of oceanography and boats is a poor analogy. The a analog to telescopes would be sonar (and maybe seismographs?). The analog to boats would be spaceships/rockets. This makes my point.
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...
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.
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.
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 ;)
This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming. That's why they are terrible for games and websites, domains where correctness doesn't matter as much as feeling and iteration speed. Sure, it would be nice if those programs had no bugs, but basically any means of increasing iteration speed and flexibility is worth it.
A startup or indie usually has a short runway. Saying we're going to half that so we can make sure we don't have any memory leaks is a laugh. It may cost 10s-100s of $K, or be the difference in launch / failure.
We basically would not have AI today if it weren't for loosey-goosey riddled-with-holes languages like python with all the symbolic madness they enable. The ability of researchers to write a few lines and run it without regard to memory, processor layouts, etc. was what enabled them to write these programs at all. Of course we've put lipstick on the pig with CUDA and torch "compiling" compute graphs, its actually such a beautiful disaster that most software runs on JS or python, two horrid languages that have so much work to make them just performant enough.
I have no idea how to go about it, but it would be very cool to have a system where you can take the soft clay approach, while having a compiler that can effectively tell what it can prove about the program, and what it can't, and as you figure out the right shape of the program, you tighten it up until you have the level of proof you're happy with.
> This is my major complaint with even less-rigid languages like rust, they kind of force you to write production-level code even if you are just brainstorming.
I will say, this was my experience when starting out with Rust, but after working with it for a while and "internalizing" it, I actually find it to be quite quick to experiment with.
Have we ever had that? The ssh-hole, the php issues, and a litany of CVEs that recently surfaced are almost all originate from bugs that predate vibe coding.
In particular, I think its deductive proofs section is unnecessarily pessimistic. People have some idea as to why their code is correct when they write it. They're occasionally wrong (at a typical rate of single-digit bugs per 1k SLOC), but you can't often write an approximately correct program without an approximately correct proof of correctness in your mind. Yes, it's true that some proofs are intractably long, but that doesn't apply to the code we actually write. A language requiring you to write out those things you're relying on and concluding isn't much more verbose than any other programming language, and that mental scaffolding makes automated theorem proving vastly easier. You'll still fail to validate correct programs from time to time, but you solve that the same way the Rust people do -- add escape hatches and/or change your code to match the solver's limitations.
Even quite complicated externalities are similarly solvable. People talk about time and filesystems and what have you as unprovable balls of mud, and ... they're right ... but that misses the point. Precious little software handles an FS correctly. That's all the level of proof your program needs; not that you never corrupt your save state, but that if no other process mucks around with your data then you never corrupt your save state. For better software (like TigerBeetle) with stronger guarantees, well, they've already written their own proofs of correctness. All that remains is tying them to the actual implementation.
But those types of programs do tend to have well-defined specifications to begin with.
Sorta depends on what type of software you're writing, and if you're interested in the topic.
But if you have a basic understanding of computational complexity and Turing machines, plus a general knowledge of basic programming and CS, you should be able to follow the article well enough to get something out of it, I think.
How often we use full int16 for counting things? Even stuff like video frames we can easily limit size_t to fixed values like `{1920x1080, 1920x1080x3 , 1920x1080x1.5, 1080}` (representing common memory sizes for 420/RGB frames).
So instead of validating the whole infinite space of all possible states, we can carve tiny tunnels in this hypercube and significantly reduce that surface of proof.
I know that in the AI era, with code being generated in enormous quantities, formal verification is important. It is effective to some degree, but in my view, software that requires provable correctness is only a subset of all software, and I agree with the author that a kind of empiricism is the right approach. Because most of it is based on understanding a customer's "requirements." And if we consider that not all requirements can be formally proven mathematically, then in practice the line between where formal verification is used and where it isn't will become clearly drawn.
Formal specification is the work of deciding where the target is, and formal verification is the work of hitting that target with an arrow. But most of software development is the work of deciding where the target ought to be. Formal specification is like shooting an arrow at a moving target and hitting the bullseye, but figuring out where to pin that target down is software development, and honestly, most of software development spends more time pinning the target's position. Especially in the AI era, even more so.
You can't formally verify code when the code hasn't even met the spec yet! It takes a huge amount of time and effort to achieve this! Even when you think you've achieved this and your code meets the spec word-for-word, some stakeholders will still disagree based on technicalities and definitions!
How in the world are we supposed to prove that code is correct when people can't even agree on the same definition of 'correct'?! That's most of the work, really.
Also, if it takes people 1 year to complete a project in such a way that it barely just meets the spec to an acceptable standard, and only in a pure high level business sense; just barely covering all the basic exception handling scenarios; how long is it going to take to add formal verification on top of that? How many more gaps will have to be plugged, how many more assumptions will need to be enumerated, in order to make your formal proof air-tight? Then what happens if the client reads your formal proof and informs you that some of your assumptions are incorrect? What value is your proof then?