The logical extrapolation of AI capabilities stress-testing human software is all bugs being discoverable. Hence, you have to aim for actually bug-free software.
The only way to do that is to make your code provable. That again is only realistically doable using AI.
In the process, people will have to turn the pretense of "software engineering" into reality, making the engineering part explicit.
That only works when humans actually understand what they're doing.
> "I have only proven [my code] correct, not bug free."
> -- Donald Knuth (if I recall that exact quote correctly)
Just because you have proven the correctness of your code, that does not mean that it is infallible. Especially -- as a lot of HN users point out -- there's intricate complexity that is likely to cause erroneous behavior if several interfaces/complexities get combined. And those might be caused, for example by a 'user' setting the driver to 'db.backend.sqlite' instead of 'db.backend.sqlite3'; and then you have suddenly an unexpected configuration.
I once saw an interview with a guy that designed garbage cans for National Parks. When asked what the hardest part of the job was he said, “accounting for the considerable overlap between the dumbest humans and the smartest bears”.
For months after some researchers “proved” our code signing system sound I was still finding security holes in the system. To this day I’m not sure what they proved. That the architecture worked? We’d already proven that to a hundred people.
This doesn't necessarily require proving everything mathematically, it also helps to design things in a way that doesn't rely on discipline to avoid gaping holes. For example, languages that allow pointer arithmetic, unchecked array access, or use-after-free have huge opportunities to make security errors that don't exist in languages without them.
A problem I frequently have with setting up testing policies is in convincing people to test what they can reliably test with the tools, and know what they cannot test.
Inconclusive tests to increase automation and coverage accomplish less than nothing. The opportunity cost, the loss of trust, the conflation of the manual testing surface area, are all worse than doing nothing.
The point of testing is to establish a level of trust. That level doesn’t need to be 100%. It can’t be 100% regardless. So you do what you can, and you solve the remaining problem a different way. But you need to know it’s there to address it, and the smoke and mirrors fight that.
I used to work for a company that enforced 80% code coverage for our CI/CD pipelines. Both teams I worked with there, in wildly different parts of the company, were playing games with excluding most files in the repo and writing dozens of tests that didn't actually test anything, just ran the code in the testing container so the lines would count as having been tested. I think LLMs have probably cleaned it all up a lot in the end, because the tests they write do actually test the code (against the code at the point you told the LLM to write the test a lot of the time, rather than a third party spec, but at least it's not just return true all the time).
Every 6 months there was a new testing initiative, which seemed to all be responded to by writing wrappers that returned true to the test automation system we were ordered to use.
> For example, languages that allow pointer arithmetic, unchecked array access, or use-after-free have huge opportunities to make security errors
All languages are built on top of an ISA, whether directly (assembler), or by mapping it to an abstract machine. The you have the dreaded “eval” function. Then because a lot of software lives on top of an OS, there’s all the virtualization that is going on (timesharing, virtual memory, filesystems,…). Memory safety is nice, but it doesn’t help you when the attacker send valid, but malicious data from a compromised source, or by exploiting a logic error.
And for kernel code, where everything is accessible to everyone, it’s much a matter of discipline, especially with so much hardware interrupts and syscalls from userspace going around. Most kernel code has very short lifecycle, it’s the data that is long lived, and it’s a shapeless blob in memory that you have to trust the other party kept in good shape.
The rule is about data structures but I feel it has wider applicability user choices in software. You should either give the user no choices, give them individual binary choices, or let them pick anything that could theoretically be valid and design your system to assume they'll sometimes pick invalid options which will need to be handled appropriately.
Here the user was the deployer and presumably owner of the deployment. An overall setup is only correct if they and the software define a setup that happens to be correct. The software is incorrect if it doesn't support the incorrect setup they require.
> The software is incorrect if it doesn't support the incorrect setup they require.
Is that what you intended to type?
Software is not required to support the requirements of every potential user. Only the ones they mean to support. That’s why Porsche and BMW ignore people complaining about how expensive they are. You aren’t their customer and they don’t want you.
A family of eight who buys a (classic) Porsche bought an incorrect car unless it is for an expensive gag like putting sugar in the gas tank then an EV would be incorrect, no?
The user doesn't have to be someone that grew up on Defcon talks and CTFs anymore though. Any Joe/Jane off the street can ask an LLM what is a JTAG or what is a 90 nop and keep asking until they're satisfied. So we have to assume the user is capable of all of those things.
Knuth seemed more interested in Tony’s notion of “obviously no bugs”. There always seemed to me to be a self-evident flavor to his literate code notions.
I say that as someone who sees Knuth as problematic in other respects starting in the 2010’s. Physics governs so much of computational complexity now that I think the idealized form he presents has transitioned from merely holding us back to being crippling. Only game designers, hyperscalers, and an esoteric few of the rest of us seem to understand the vast gulf between theory and practice that has developed in the five orders of magnitude that compute power has experienced since his first edition.
Many, many things that are considered constant in his world are instead logarithmic to the size of the data being managed, or in the case of very large data sets, order n^1/2 because of speed of light and thermodynamics. That vastly reorders the toolbox, because second shelf algorithms now rival or beat the top shelf ones and some options even farther down now become interesting for novel situations.
Regarding your remark "[...] because second shelf algorithms now rival or beat the top shelf ones [...]". That is honestly something I would never have believed back in the 2000s, Windows XP era:
I thought we needed more than the classic mathematical operations and if/else for an operating system that drives the modern world like it had been envisioned by sci-fi in the past 100 years.
That turned out to be wrong: Your modern android with a couple of simple apps is everything a man from 1900 might ever conceivably want from technology.
And it is all if/else/while and mathematical operations.
It turned out you just needed enough of these, to get everything working nicely.
Maybe that says something about kubernetes. Software systems that are complex enough to be intractable should probably be regarded as too complex to operate safely.
I don't fully understand what you're objecting to. Are you saying it's not possible to build a formally verified container orchestration thing?
I do think that most software out there is unsafe. That doesn't make it useless, but if the effort required to exploit vulnerabilities is decreasing we will probably need to stop building things that way.
Which implies that software engineers in the future won't be so cavalier in allowing mod-able or unix-like systems. There won't be an db.backend.sqlite since your software likely won't use a db, and if it does it will be a custom design. It won't be "if several interfaces" it will be "there are no interfaces" no programmer interfaces and certainly no user ones.
> The only way to do that is to make your code provable. That again is only realistically doable using AI.
I think that LLMs actually cannot do this right now while people can?
Also there is a lot of defensive programming that has been left to application and runtime layers because of dated security models in our OS and permissions that are way too coarse. It's a lot easier to write a correct program when you don't have to check every path and do that perfectly when the permission system can ensure that no files that haven't been whitelisted cannot be read
My intuition is the opposite? The math results we are seeing lately are done with theorem provers. LLMs are getting very good at this and surpassing what humans have been able to prove. Verified code is traditionally very expensive and only applicable in niche areas when done by humans.
> LLMs are getting very good at this and surpassing what humans have been able to prove.
But if the reverse were true it would be impossible to prove. AI is trained on all of humanities solutions - LLMs stand on the shoulders of giants, not the other way around.
As of today, the training data the originates from humans represents a vanishingly small portion of the total training. The vast majority of training - how many 9’s is a trade secret - of a frontier model is synthetic RLVR data. That’s how they got good at this.
LLMs can, in principle, do everything humans can. And arguably more. "Right now" is how long? People are slow.
"Provable" essentially means, you have explicit operators acting on explicit states in an exhaustively defined way that preserves "truth", explicitly defined invariants.
A finite thing you can argue over deterministically.
Obviously, "you" there is an LLM, the machine your code is run on has to be defined in that very same exacting manner and so on.
That still isn't enough, you need abstraction, a hierarchy of categories that preserve your intent and accurately describe the problem space.
"Programming" then is solving an inverse problem over that hierarchy, filling in the blanks sensibly on your way down through the model hierarchy, all the way to atomic instructions your (proven) hardware understands.
Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.
All of which is to say: yes, the current state is a mess. Resolving that is far from easy.
But you really have no choice, that mess is transparent to large-enough LLMs. Security by obscurity only goes so far.
> But you really have no choice, that mess is transparent to large-enough LLMs.
It's transparent to large-enough LLMs given enough resources. Which is the thing that was always true. The difference now is that the level of resources is lower, so we're finding a bunch of things it wasn't previously economical to find.
But the cost still isn't zero. On top of that, the same LLMs are now generating enormous volumes of new code, which both nobody has verified to that level of exaction and nobody has even considered how it interacts with existing and other new code.
> Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.
This I can agree with, and my perspective would be that we have theoretical solutions with no ergonomics, and rely on unproven (as in formally proven/validated) mechanisms. WASM + capability passing is enough, but the WASM layer is still built on an OS or runtime that is not proven and you'll have a heck of a time trying to build a product on it
> LLMs can, in principle, do everything humans can.
Oh yeah? slides baton Pick up that can, Clanker.
Jokes aside, I do want to see the first news of AI going out of its way to acquire and make use of actual currency and hiring a meat proxy. I don't even care what for, can be making paperclips.
While I whole-heartedly support the goal of actually bug free software and treating software engineering as a serious engineering discipline, as an experienced software engineer who also studied physics, I have to challenge your base premise about what it means to make engineering explicit.
Namely:
> The only way to do that is to make your code provable.
Proofs are a mathematical concept. They only work in the abstract world of mathematics where everything is perfectly logical.
Engineering exists in the real world. The physical realm where our mathematics are only imperfect models of what actually exists. Removing bugs through physical engineering requires persistent trial and error until you have found all the places where our mathematical models don't adequately represent the real world.
It's the same in software engineering, which involves cobbling together a myriad of systems not all designed to talk to each other and massive, ever changing codebases where perfect knowledge is impossible.
So yes, we should be trying to engineer bug free code. But that's really more a matter of changing our resource allocation, spending more time and money on QA and doing away with mottos like "Move fast and break things". It's a cultural shift and will only come when the bosses -- the venture capitalists who ultimately control our industry -- are held accountable when things break, and given strong incentives to ensure they don't break.
Back when I worked at Boeing, I was encouraged to get a PE license. I looked into it. I was not impressed with the exam (it was too basic), nor the requirements, and so did not bother.
The legal framework for software liability is tightening. The Cyber Resilience Act is one such example that forces developers to get their act together.
> It's a cultural shift and will only come when the bosses -- the venture capitalists who ultimately control our industry -- are held accountable when things break, and given strong incentives to ensure they don't break.
The problem here is that the correct amount of resources is context-dependent.
Suppose you're a small business and you're putting up a website to display the menu for your restaurant and directions to get there. Do you want it to get compromised? Of course not. Does it matter very much if it does? Eh. Should you spend $50M in formal verification to make sure it doesn't? Definitely not.
Whereas if you're developing the software that keeps planes from falling out of the sky, that's an entirely different context.
The problem comes when someone grabs the awful WordPress junk that was suitable for displaying static menus and wants to use it to process credit cards. But even that isn't really the fault of the awful WordPress junk, it's the fault of the credit card companies for designing their financial technology in such a ridiculous way that Merchant A has to be given a secret that allow purchases to be made against the same card at Merchant B, instead of using the decades-old cryptography that would prevent the customer from ever needing to give anyone a secret that enables that wide a scope of compromise.
It comes down to how much work is justified to ensure that the thing not have problems, which is not at all the same across different domains.
The physical world is actually part of mathematics. Look into John Archibald Wheeler and his "It from bit". In particular, the physical world is finite.
Therefore, mathematical proofs very much apply to physics.
You're right about approximations: we gather data and improve theoretical models in an attempt to exhaust that complexity reality poses.
You're wrong about exhaustive knowledge about codebases being impossible. LLMs enable exactly that.
The trick then is to transfer that knowledge in a usable way to what we know about the codebase.
Keep in mind, a mathematical proof is just "an argument that convinces a mathematician".
It doesn't actually give you the truth of a statement, it just convinces a mathematician of its truth.
That doesn't actually change when computers are brought into things. You can convince a mathematician that an automatic theorem prover constructs correct proofs with another proof, but it's "I think this looks right" all the way down.
No, you're incorrect. A mathematical proof actually is a program by the Curry-Howard correspondence.
Mathematicians are trained to act as the compiler, verifying the code, doing the type checks, and to a degree the state machine "running" those programs.
Human mathematicians use introspection to tell you whether a proof/program does what it is supposed to do. They keep those programs small enough to be run on human brains by modularization, abstracting away complexity behind defined interfaces. They mostly rely on other mathematicians to have checked those sub-modules properly.
By defining that state machine, compiler and the tree of "all" known proofs as programs explicitly on a computer, you get Lean and the according libraries of verified proofs.
A proof-program there is verified when it compiles and passes the deterministic structural type-checks built into the language while fulfilling the requirements stated for its interface.
It all reduces to a few thousand lines of trusted code, the Lean kernel, being correct. It's mostly what humans do too, but actually considerably more thorough.
Engineering is the discipline of designing and implementing solutions that achieve desired outcomes, using limited resources, while satisfying a defined set of constraints and minimum acceptable standards.
We have way more resources now to achieve way higher standards.
As a general rule, building things as an engineering project (according to engineering, whatever you want to call it) doesn't prove they work. Rather, it proves they don't fail in specific known/defined ways. There's always ways they can fail that aren't known/checked, and frequently ways that aren't considered important.
Kind of like automated tests in software development. Except the people that pay for the engineering stuff are more likely to pay for the extra tests, because of liability.
Engineering is the application of science and mathematics to solve problems and create solutions… that “application of science and mathematics” is what’s been missing from the majority these last 20 years.
I don't think so. The article refers to formal verification, but also notes that proof checking should be done by humans. We don't have enough capable humans for that.
Looks like AI is finally proving Linus's Law[1]: "given enough eyeballs, all bugs are shallow"
Open Source was supposed to prove this, but as it turns out, there weren't enough human eyeballs, and those eyeballs weren't looking for bugs. LLMs eyeballs see the entire codebase at once.
> That again is only realistically doable using AI
The opposite. The amount of bugs that I've seen AI add to software is tremendous, some bugs are things that even a 18 years old that starts working as a developer right after school wouldn't do.
Also they are unable to fix them, if you ask them to fix a bug they probably introduce 3 other more, and so on, and you arrive quickly at the point that the code is a mess of spaghetti that needs to be rewritten completely (by a human, this time).
On the opposite side AI is good at finding bugs, so I use it more as an advanced linter that tells me if I'm doing something wrong.
You’re describing vibe coding and GP is describing systems for proving correctness.
If you ask an AI to generate a novel math proof, it will inevitably produce garbage. If you give it the tools to do this (e.g. Lean), evidence is that it can in fact generate meaningful proofs.
To the extent that we cannot prove software correct, this is probably largely a tooling problem.
“tooling problem” makes it sound trivial, its a tooling problem like building a quantum computer is a tooling problem. Ie something that probably won’t be solved in our lifetime
> something that probably won’t be solved in our lifetime
If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.
I don’t know what it looks like to get to fully provable code, but I don’t see that it’s fundamentally impossible in my lifetime. Especially depending on scope. Will an entire operating system and everything on it be fully proven correct in my lifetime? Maybe not. Could the authentication stack for a product be entirely proven correct? Sure. I can’t believe that.
> If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.
A single PC can solve a very complex simulation model in seconds, something that would require years using humans to do. Same as solving a very complicated maze. So if coupling a text generator with a proof verifier is now capable of coming up with a proof, I’m not particularly surprised. But given the cost, and the actual usefulness of the proof, I’m not particularly excited either.
But code is not a closed system, even if we do prove a lot of the internal mechanism, we still can’t know the input (noise), and whether the axiomatic foundation will hold. That’s the reason people don’t bother. The theory of computation is just too loose in its constraints. You just write enough tests to catch egregious errors.
"Software" might not be, and definitely not software systems -- but code can have each part of it atomically proven to be correct, assuming you test it with a sufficiently complex simulation model (which you've already granted is within the possibilities for LLMs).
Prove all the code in the software system correct, then prove their interactions are correct, and you've achieved your goal.
(I won't claim this is inevitable with the current tools, but it's at least within the realm of possibility)
What model are you talking about when you say this? "AI" is not one thing, and if you think frontier models are at all comparable to a typical 18yo SWE, you've never actually worked with one of those two.
Most bugs are not security issues and most potential security issues aren’t exploitable. So you can have plenty of bugs in your code without getting hacked.
> The logical extrapolation of AI capabilities stress-testing human software is all bugs being discoverable. Hence, you have to aim for actually bug-free software.
> The only way to do that is to make your code provable. That again is only realistically doable using AI.
If you're code is "provable" doesn't that only mean you've proved the code meets its specification? The specification can still have bugs.
Yes, that's where the "engineering" part comes in.
Engineering builds models that approximate the real world under practical considerations. You e.g. have to weigh costs vs risks and apply good judgement.
In essence, you try to achieve the best possible with the resources you've got.
You are describing the difference between Verification (Does this do what we explicitly said it would do?) and Validation (Does this do what we wanted to achieve?). One is about compliance of design promises, and the other covers the issue that the various levels of design documents might have failed to completely capture intent.
Depends which way you mean. It is possible to provide a formal specification for a proof verification engine and prove, in the same language that the engine is for, that the engine implements that specification.
Proving that the system it implements is like, logically sound, is a different issue, and for that you do need stronger axioms.
On the contrary - this is explicitly the mission of most military organizations. There are countries in the world today where every day their bridges and buildings face adversarial attacks from state level threat actors.
The difference is, people who build civilian bridges and buildings are not actually generally expected to build structures that can withstand such attacks because preventing those attacks is considered the government’s job.
So no, they typically don’t undergo ‘more rigorous testing’ than software against security threats. The fact that governments make no effort to protect networked systems from being attacked places the burden of withstanding those attacks fully on the private civilian operators.
In an important way bridges and buildings are indeed proven to be sound by applying the mathematical tools of structural engineering, materials science, etc. Software Engineering also has analogous formal tools at its disposal (Lean is one gaining a lot of exposure these days), but many were being neglected because it wasn't worth the bother. In this new adversarial world, we'll be forced to reach for them more often. Luckily the models are also a big help in making these tools more approachable.
The only way to do that is to make your code provable. That again is only realistically doable using AI.
In the process, people will have to turn the pretense of "software engineering" into reality, making the engineering part explicit.
That only works when humans actually understand what they're doing.