Hacker News
points by Quimoniz 3 days ago | 0 comments
> "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.

[–] phorkyas82 3 days ago
Were you aiming for this? “Program testing can be used to show the presence of bugs, but never to show their absence!” ― Edsger W. Dijkstra

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

[–] raphlinus 3 days ago
No, it's Knuth. The exact quote is "Beware of bugs in the above code; I have only proved it correct, not tried it." [1]

[1]: https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf

[–] Loquebantur 3 days ago
Yes, you can also easily prove the wrong thing.

That's why it doesn't suffice for only LLMs to know the relevant stuff.

You can't have a zoo run by animals.

[–] Revanche1367 3 days ago
Aren't all zoos technically run by animals? :D.
[–] gfody 3 days ago
apt, as we try to contain the complexity of our designs while being ourselves panarchical hyper-systems
[–] sach1 3 days ago
Unrelated but "Panarchical Hypersystems" makes for a great company name
[–] devonzh 3 days ago
Or a rock band. (With a nod to Dave Barry.)
[–] 59percentmore 3 days ago
Dovetails with it sounding like a secret society/esoteric superweapon monopoly corp from a Daisuke Ishiwatari joint.

On that note, "Esoteric Superweapon Monopoly Corp" would also make a great band name.

[–] prcrstntr 3 days ago
Lower intelligence animals....oh wait
[–] LeFantome 3 days ago
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”.
[–] hinkley 3 days ago
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.
[–] socalgal2 3 days ago
Correct, because when there was no LLMs all code was perfect and bug free.
[–] ourmandave 2 days ago
Just because you have proven the correctness of your code, that does not mean that it is infallible.

Can god make a zero-day even he can't find?

[–] ElectricalUnion 2 days ago
Most bad crypto code in the world is unbreakable by it's creator.
[–] svachalek 3 days ago
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.
[–] hinkley 3 days ago
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.

[–] annzabelle 3 days ago
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.

[–] hinkley 2 days ago
I’ve seen that behavior but it usually doesn’t kick in until the mandate 90%, so that’s a shame. Usually I push back on it being a rule because if you have low coverage, you have a team that’s not good at automated testing, and forcing them to write a lot of tests before they’ve gotten good at it always ends poorly. But typically nobody listens and the shitshow begins.
[–] latentsea 3 days ago
Seems like a culture problem at both ends of the org.
[–] hinkley 2 days ago
It’s a pretty common failure mode in my experience. Keep management out of testing as long as you can.
[–] latentsea 2 days ago
Keep shitty tests out. PRs with vacuous tests should be rejected. You can have high coverage and good tests. These aren't mutually exclusive.
[–] gopher_space 1 day ago
Demonstrate the good vs bad test cases to people by doing an obviation pass over your test suite. Lots of things to look for, like misunderstanding the flow of data authority or testing against things that are fundamentally Somebody Else's Problem.

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.

[–] skydhash 3 days ago
> 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.

[–] eru 3 days ago
Using these languages is pretty close to a mathematical proof.
[–] jopsen 3 days ago
Play a bit with it, I started feeling like verification is just a slightly more aggressive fuzzer.

There will also be compiler bugs, etc.

The point is fewer bugs.

[–] kolinko 3 days ago
At least in some cases it is easier to verify bytecode/assembly than source code.
[–] hinkley 3 days ago
Just because it works doesn’t mean it’s not broken.

Anyone who has ever wielded a wrench should know that implicitly.

[–] MisterMunchkin 3 days ago
If the user is capable of setting an option which breaks everything then your code isn’t correct.

That’s the whole point, you can find all of these things which would take far too much manual effort.

[–] wolrah 3 days ago
The zero, one, infinity rule isn't directly relevant here but it's close enough to be worth mentioning IMO.

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.

[–] telebub 3 days ago
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.
[–] hinkley 3 days ago
> 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.

[–] telebub 3 days ago
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?
[–] hinkley 3 days ago
As written you have stated that Porsche is wrong for ignoring this family's complaints. Because they didn't support an unsupported configuration.
[–] telebub 3 days ago
You are confusing the wants of a manufacturer with a system that is being used by a person. The person owns the system that is either correct or incorrect for their needs and the manufacturer takes money and screws off. Or, you have the "soup Nazi" as proposed with the manufacturer makes sure you use the system as they imagined and not with a database setup beyond their control.
[–] timschmidt 3 days ago
The user may be capable of undervolting the logic, issuing directed EM attacks, accessing JTAG, etc. Good luck.
[–] solyin 3 days ago
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.
[–] wizzwizz4 2 days ago
We used to have these things called "books" that you could ask. (And if you didn't know which book to consult, we had these people called "librarians".) I don't think it's a much greater threat surface than before: if anything, it might be smaller, because the internet is harder to search.
[–] timschmidt 2 days ago
As someone who grew up with libraries, card catalogs, microfiche, and an encyclopedia, I can confidently say that talking to and working with an LLM is much faster, much easier, and much more informative than all of the above combined.
[–] eru 3 days ago
> Just because you have proven the correctness of your code, that does not mean that it is infallible.

Yes, but it gets you pretty far already.

[–] casey2 3 days ago
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.
[–] moomin 3 days ago
I mean, he wasn’t using, or even envisaging, a language that could natively support proofs.

Personally I think proving Kubernetes, for instance, would be an exercise in pure frustration. There’s just too much to do.

[–] hinkley 3 days ago
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.

[–] Quimoniz 3 days ago
huh. Interesting background. Thanks for sharing.

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.

[–] 27183 3 days ago
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.
[–] devin 3 days ago
[–] 27183 3 days ago
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.