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.
[–] Loquebantur 3 days ago
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.
[–] saalweachter 3 days ago
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.
[–] Loquebantur 3 days ago
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.
[–] bathtub365 3 days ago
[–] joshheitzman 3 days ago
But there wasn't enough demand and it was discontinued.
[–] gmueckl 3 days ago
[–] WalterBright 3 days ago
[–] IAmBroom 3 days ago
"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.