Hacker News Reader

Comment by jeanpah | Hacker News Reader

Do You guys think that with ai we Will achieve something like a bug free os distro or programming language? Like some sort of perfection?

View on HN

From just writing code, no.

Now, the question is can we make some kind of formal verification language that forces checks everything and doesn't allow bugs? Maybe?

But that's assuming the underlying hardware and firmware doesn't have flaws that can break those assumptions too.

That just shifts bugs up one layer, into the specification that you then verify

Yes but that is significantly less surface area (indeed asymptotically less in the general case if you believe P != NP).

I remember languages like Casl and vdm, But they where harder to implement and very complex, You mean something like those languages ?

>But they where harder to implement and very complex

This is the general trade off for being correct. Being mostly right is easy, but leads to complex security issues later. Being correct is very hard, but should reduce the number of flaws to a manageable level.

I think Lean or Ada would be examples of different types of correctness contracts.

I remember those languages were used to verify an implementation, in space rockets code (uni teacher said). But maybe there is a way to build something perfect instead of veryfying the correct implentation?

There are two different layers here. You have the binary layer, where software is written and works at on a theoretical level. Then you have the messy components that interact with reality at an analog level. This is why one of the first tenants of security is don't give anyone else access to your hardware.

But even that isn't a foolproof winning strategy. When you start digging deeply you realize we exist in the allegory of platos cave. The reality we experience is an emergent phenomenon related to the scale at which humans operate. Things that operate at a much smaller scale experience a completely different reality than you do. For example gravity becomes so insignificant it's like it doesn't even exist when you're small enough. At least for me it's not hard to imagine nano machines that infect the substrate of a CPU and farm all your secrets out on side channels, or any number of other things that are pure sci-fi at the moment.

I think we can get mostly there with AI and bug bounties. I think we're right in the middle of "peeling the bandaid off" right now. The code released in the near future will have the same opportunity to run through the 0-day gauntlet. So if it contains exploitable bugs, they generally could have caught them. Sweeten the deal with cash and you can outsource most of that.

I can only think of Edsger Dijkstra's quote: "Program testing can be used to show the presence of bugs, but never to show their absence [...]". Adding that computers are mathematical models and Gödel's incompleteness theorems stating that a system cannot demonstrate its own consistency, I would say that it is likely that bugs/errors will always exist.

The theorem can be used un this way? Wasn't only for natural numbers? You argument seems solid if thats how the theorem works. Maybe there is a way not to find Bugs but to build things perfectly from the start.

My understanding is that the theorems apply to any "formal systems". If my assumptions of computers being part of "formal systems" is correct, then the theorems should apply, per my understanding.

No, but languages like Elixir/Erlang/OTP are designed to fail gracefully while continuing to run.

With complex systems there are too many failure modes, and with "vibe coding" institutional negligence it is simply degenerative.

There are theoretical workarounds to LLM brute force scans, but they are not free to build. =3

I think AI might make reimplementatiion from first principles more viable (think: an Oberon os with Linux driver support; or: a full environment like STEPS, but for real use) - which might make it feasible to simplify the problem domain (firmware, driver, os, UX, compilers) - to the point that it becomes easier to create bug free domains/subsystems.

Technically, if the rate of bug detection and correct bug fixes by AI is larger than the rate of newly introduced bugs by humans & AIs, then we'd asymptotically approach a bug free OS in the long run. But these are big ifs.

Definitely at best a "sort of" type perfection. The endgame here is formally verified everything, at which point the only question is whether the then-consistent model that's implemented is any reasonable in practice.

Think "this is not a vulnerability, as no security boundary is being unexpectedly crossed" except the way the security boundaries are laid down is utterly stupid and hilatiously nonsensical. Same for non-security related defects ("working as expected, wontfix" -> "the way it works is dogshit, and so your expectations are idiotic too").

Now, since these things are supposed to align with human sensibilities and are supposed to capture the human semantic understanding of our world, theoretically, this should still leave us in a pretty good spot. But not a guaranteed good spot, as that is not actually tractable, ever, and fundamentally so.

Thanks man, You said it perfectly, The software can be prefect,but us as humans can't, and that will lead to problems with the software.

You could just implement a virus perfectly and the wrong bussines process.

Vendors will just redefine the meaning of bug if needed.

Everything is bug-free until someone finds a bug in it.

Not as long as new features are being written.

lmao

One can dream

Reply on news.ycombinator.com