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.
If a new jet completes extensive flight testing and has flown around the world but has undiscovered engineering flaws, “it’s working”.
Meeting verification and validation requirements in a sound engineering development program should certainly get you to “it’s working”, whether there are undiscovered engineering flaws or not.
Anything men build is subject to failure and unknown unknowns - so nothing works?
> -- 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.
That's why it doesn't suffice for only LLMs to know the relevant stuff.
You can't have a zoo run by animals.
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 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.
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.
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.
A base exercise in this vein would be asking someone to describe how a failure state they're checking for could come to exist in your current system.
That’s the whole point, you can find all of these things which would take far too much manual effort.
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.
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.
Anyone who has ever wielded a wrench should know that implicitly.
There will also be compiler bugs, etc.
The point is fewer bugs.
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
Yes, but it gets you pretty far already.
Can god make a zero-day even he can't find?
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.
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.
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.
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
Folks are creating some interesting stuff in this space
"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.
I think narrowing the scope of this statement would better support your argument, as it is easily disproved in its current form.
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
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.
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.
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.
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.
Extreme naivety alarm... Explain how code provable allows for bug free software. Would love to understand the intellectual jump there.
The quote captured the fact that a human reviewed proof could have mistakes in it. This is very different from a Lean verified proof.
Proving that the system it implements is like, logically sound, is a different issue, and for that you do need stronger axioms.
Clanker doesn't care it's boring or too much work. Clanker just grinds 24/7.
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.