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.
> -- 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.
Can god make a zero-day even he can't find?
Or the second one, that I would have attributed to Dijkstra, too: “There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies and the other way is to make it so complicated that there are no obvious deficiencies.” C.A.R. Hoare, The 1980 ACM Turing Award Lecture
That's why it doesn't suffice for only LLMs to know the relevant stuff.
You can't have a zoo run by animals.
On that note, "Esoteric Superweapon Monopoly Corp" would also make a great band name.
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.
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.
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.
There will also be compiler bugs, etc.
The point is fewer bugs.
Yes, but it gets you pretty far already.
Anyone who has ever wielded a wrench should know that implicitly.
That’s the whole point, you can find all of these things which would take far too much manual effort.
https://en.wikipedia.org/wiki/Zero-one-infinity_rule
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.
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.
Personally I think proving Kubernetes, for instance, would be an exercise in pure frustration. There’s just too much to do.
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.
Watching in awe. Watching in awe.
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.
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
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.
"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.
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.
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
I think narrowing the scope of this statement would better support your argument, as it is easily disproved in its current form.
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.
Folks are creating some interesting stuff in this space
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.
But there wasn't enough demand and it was discontinued.
"I decided for myself that X wasn't worth me pursuing as a path for my career." Good for you.
I made the same decision for professional photography and cardiac surgery, but both of those careers still hold value to society.
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.
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.
I agree with the necessary cultural shift.
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.
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.
We have way more resources now to achieve way higher standards.
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.
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.
The quote captured the fact that a human reviewed proof could have mistakes in it. This is very different from a Lean verified proof.
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.
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.
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.
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.
Doesn't matter. Just like you can prove something is true for all numbers, you can prove something is true for all possible inputs.
Code is absolutely a closed system.
"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)
> 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.
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.
Clanker doesn't care it's boring or too much work. Clanker just grinds 24/7.
Proving that the system it implements is like, logically sound, is a different issue, and for that you do need stronger axioms.
Extreme naivety alarm... Explain how code provable allows for bug free software. Would love to understand the intellectual jump there.
But also I would bet those undergo more rigorous testing than a lot of software.
Airplanes have much smaller safety margins, meaning a lot more calculation is done, and there's a high emphasis on double checking everything.
Spacecraft have tiny safety margins, which amps up the design rigor to 11.
When terrorists take the control of a plane, it's a catastrophe.
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.
I'm skeptical; every line of code is a liability. Humans regularly make the trade-off between adding lines of code vs doing without the incremental feature addition. LLMs don't; everything gets added.
The recent brotli attack should have been a wakeup call - few people use it, no one actually needs it, but the exploit that it carried was present on every system. Everything from IIS to Caddy and in-between, and yet no one was actually using the thing.
It's a liability to add code, whether you're duplicating existing code in the codebase or adding a feature 1% will use.
LLMs can run with whatever directive you give them. If the directive is lots of code that's what you get. But when everyone gets repeatedly burned by vulnerabilities the directive becomes building bullet-proof code. With the right prompting an LLM can be a lot more diligent about that than we ever could.
It might be true but it's also a pointless statement that doesn't impact the problem, because it won't happen. And "it won't happen" isn't some unsupported prediction that no one can say. The aggregate behaviour of humans is a known thing, and it's not productive to the actual problem to pretend otherwise. It's only productive an individual looking for an easy excuse to avoid dealing with the problem.
By default, yes. But you don't have to let them, and enforcing some code quality was shown to use significantly fewer tokens (can't find the link now).
I could have worked through all that on my own, but having the AI as a rubber duck to talk to - plus the edge cases it was able to point out - was really helpful.
I wonder if a refactor is even necessary.
Concepts like KISS, DRY, etc. are largely human-centric. They're meant to make code easier to write, understand, and maintain - for people.
Duplicating code was traditionally "bad" because it increased maintenance costs, risked divergence, and added cognitive overhead for human developers.
But with coding agents, some of those tradeoffs start to change. An agent can find and update duplicate implementations in seconds. It doesn't need to maintain the same mental map of a codebase that a human does.
And if we have good specifications and comprehensive tests, behavioral divergence should be detectable and correctable. In fact, duplication can offer an advantage over shared abstractions: isolation. Changes to one implementation don't risk breaking unrelated consumers of shared code, and each implementation can evolve independently.
Maybe we won't need as many high-level abstractions, or eventually even some of the architectural patterns we consider best practices today.
If the cost of writing and maintaining code approaches zero, perhaps we should optimize less for human readability and more for runtime performance, memory efficiency, isolation, and correctness.
We might even regain some CPU and memory efficiency by eliminating layers of indirection, virtual calls, and abstractions that primarily existed to make code manageable for humans.
Perhaps the optimal architecture for AI-maintained software is fundamentally different from the optimal architecture for human-maintained software.
A lot of our software engineering best practices are based on the economics/ergonomics of human maintenance. What happens when those fundamentally change?
Until proven wrong by coding agents, this is still the case even for agents. Not sure why you are assuming this doesn't apply for the machine
I cannot read a 50K LOC code base at once. I mean, obviously, I can physically do it, but I don't have the patience, etc. I need mental shortcuts like abstractions layers to hold even parts of the code base in my head. LLMs don't. They can read that in seconds and hold the whole thing in context.
The models don't know that they're not human when they estimate. It's worth telling them that all estimates need to be made in the context of an agentic AI doing the work.
Now, I wonder if it actually agreed, or if it sensed that I preferred the robust solution and was trained to make me happy.
Same with any other acronyms - if you don't set up guardrails on when given principle should apply you'll get code that you can only complain about.
Oftentimes there are two broad ways to fix a gap in the logic. You can eliminate the source of it, which often involves refactoring but tends to result in less code and cleaner, more comprehensible logic. Or you can leave the gap there, but attempt to render it safe by adding extra logic to detect and handle the error condition. This reduces changes to existing code, but makes the overall system more complicated.
You can’t just indiscriminately favor one approach. Which one of those is best depends on the situation. The deciding factor is often something like a time constraint that you can’t know just by reading the code. You might need to talk to your team before deciding.
But LLMs don’t do that. They always choose option B: slap a bandage on it. Keep on adding more epicycles. In the 2000s we learned that, over time, always choosing this approach inexorably leads to codebases that are brittle, bloated and expensive to maintain.
So the problem, from my perspective, isn’t that we shouldn’t be coding defensively. It’s that LLMs encourage us to do it in a way that we’ve already learned is unsustainable.
I don't think this is anything new, nor LLMs are to blame here. Although - LLMs want to make you happy, or maybe they don't think about what user actually needs, just how to accomplish the goal that was stated; they do stuff without asking questions (unless you constrain them or plan first). I've actively put in a hook for my agent to not make decisions on their own and ask me when it detects it's about to make a decision.
I think where a lot of people run into problems with the KISS principle is they conflate simple and easy. More often than not, simple is hard. Which is maybe a soft reason why agentic coding, which is all about trying to make every task easy, leads so consistently to complexity and bloat.
If you write your prompt as a request, and not carefully as an idea or suggestion, the bot can blindly agree to 'help'. And if you are stubborn about it, you can lose hours on something that cannot work, or make the code infinitely worse.
However, it's also the path of getting better at programming. To learn to take a step back, to ask yourself if it's really sensible. Just that now it also involves questioning the bot's help, as well as writing your prompts to prevent it.
Not coding for situations that “do not happen” is exactly what creates vulnerabilities. But I also don’t think that such code is the main source of complexity in LLM-generated code.
Having it in the lower layer is correct, a proper optimizing compiler should be able to detect there's a single code path to the function and that the checks have already been done, skipping the second check.
[1]: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
That’s why I think code needs to document all its assumptions, and in a way that is checked by the compiler to the extent possible. If you document that the values have restricted range, then the AI should be taking it into account.
My main point still stands = LLMs code defensively catering for unknowns that are not loaded into context.
Yet, I removed 2/3s of the code, because it triple-checked that every file really existed and was valid, that the input form was less than a million bytes in size, that there were propper HTTP status codes for everything, that every possible error from reading data was eagerly checked and caught, and so on.
Like come on, three people will ever look at it. So keep it small and tidy so I can understand it better!
i am going to quote that a lot...
We don’t have effective objective measures of what would constitute KISS.
Impossible for you, me, and other humans maybe. But not hard to understand for LLMs
> I want to see an LLM reduce a complex multi-million line codebase to 1/10th of its size or less without breaking functionality. That would be impressive!
They can and do, if you ask them to.
If you have tests to validate functionality, it can easily reduce and refactory.
But, why are we caring about LOC again?
To me KISS is basically about how you’d write the code, the architecture, which is something that - at least currently - humans need to oversee when writing new code with LLMs.
But what does it have to do with AI discovering a ton of bugs in a lot of (open-source) software?
Maybe, when they build a pomodoro timer, people will consider the possibility that the entirety of a browser engine as well as 30 000 javascript dependencies from random unvetted sources introduces unnecessary complexity and a practically infinitely fractal attack surface.
Someone not following KISS, might install Windows Server + tons of bloated applications, in order to serve a .asp server, which serves JSON that never changes, or something similarly stupid.
Meanwhile, the KISS developer would put static .json files on a CDN or self-hosted Varnish or whatever, and call it a day.
The first opened up a whole can of potential venues for exploitation, while the second might only have opened up one potential venue for exploitation.
That doesn't mean every simple system solves the problems we intend for it to solve. It means that all else being equal, we should prefer parsimony.
It is also unfortunate than in more than half the cases where AI provides a 'fix' that fix breaks something else, so my guess is this is going to be 90% human labor to correct, at least initially.
A complete plan to reduce vulnerability from untoward influences is more feasible now with agent assisted engineering. You have to be carefully selective about what matters and what doesn't, or the cost and time balloon out of control.
I don't see China antagonistic to the west - they want autonomy, and don't share many of the values, but they're open to a wealthy West spending lots of money in Chinese goods.
Russia, at least its government, is a bit more, especially recently. But anyway, why reinvent the wheel when a battle tested FOSS is there for the taking?
One does not simply "write a browser"...
HTML is entirely the wrong comparison as it's a document format and not a programming language, and "as long as you can write a browser" is not a simple condition. Do we have any browser (even in development) that isn't written with current toolchains? Or a headless javascript runtime perhaps?
But I also don't understand why (without compatibility layers) a browser should be as complex, or remotely as complex, as currently, specially with all the knowledge in hindsight.
I'm not saying this is easy, doable, or whatever, but that was what I meant.
I predicted long ago that when computers become totally secure intelligence and LEA will lobby for mandatory backdoors, possibly through secret courts.
in the beginning, ppl didnt know a lot, and default passwords and stack overflows were 0days.
then awareness came and a lot of that is actually fixed. Writing a modern exploit more often now requires many stages and a shit ton of skills and knowledge.
that will increase.
nothing will be 'fixed' in that utopian sense.
NSA spent 20 years stockpiling vulns and pushing the industry towards half-assed solutions like address sanitization and pointer tagging when they could have put the industry on memory-safe languages instead.
They managed to get the IME/PSP/TrustZone into 99% of the CPUs out there by mandating it for government purchases; they could have done the same thing with memory-safe languages. But instead they chose to stockpile vulns. Hope they burn in hell for this.
Even if they wanted to, I highly doubt they could push the industry to do that. The industry does what it wants to do, and rewriting tons of software was far from its priorities. There were no LLMs back then to help with such a massive migration.
There's also the fact that rewriting software tends to introduce a lot of new bugs.
Memory safe languages are not a silver bullet either.
Basically, the borrow checker allowed writing memory unsafe programs without using the keyword unsafe.
Compilers for C, C++ etc. are well established but Rust is a relatively new language. There are many bugs to come just like this.
Using a memory safe language is not a silver bullet for writing memory safe code. The implementation of the memory safe language introduces bugs as well.
I'm saying that these compiler bugs are extremely low on our list of priorities. If we want to eliminate all vulnerabilities in all of software we have about a century worth of logic bugs that are likely more critical and easily exploitable than compiler bugs.
The distance between the usual consumer/b2b tech startup and the kind of company that sells software to the air force is even bigger than the distance between Google and the kind of company who hires Accenture.
Yeah, about that. Its the biggest vulnerability in the industry. Nobody wants to confront this fact, though.
Too much profit to be made in subversion and human rights abuses.
" In 2013, The New York Times reported that documents in their possession but never released to the public "appear to confirm" that the backdoor was real, and had been deliberately inserted by the NSA as part of its Bullrun decryption program. In December 2013, a Reuters news article alleged that in 2004, before NIST standardized Dual_EC_DRBG, NSA paid RSA Security $10 million in a secret deal to use Dual_EC_DRBG as the default in the RSA BSAFE cryptography library, which resulted in RSA Security becoming the most important distributor of the insecure algorithm. "
People seem to be fine with it as long as their own team seems to be profiting from it - but for those of us who are not subject citizens of the NSA's government, it is a truly heinous state of affairs.