Hacker News Reader

Comment by lutusp | Hacker News Reader

> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.

I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.

The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.

The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.

For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?

View on HN

The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."

> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.

> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.

That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".

> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."

I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.

The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.

> The language is Turing-complete, not the program.

That means we can't make the claim that a particular program, running in that language, is error-free. I don't get why people find this so hard to understand.

> That would imply you could never know anything about a program.

No, it means we can't make the claim that a program is error-free. That's the simplest statement of the Halting Problem.

When someone applies Lean to verify the correctness of a chain of logic, they must remember than Lean cannot be proven to be error-free, because ... wait for it .. Lean is Turing-complete.

I think incompleteness theorem means that you can't guarantee the agents will always be able to converge on a proof, since you can't have both completeness and soundness (and we obviously need soundness since that's the whole point of a theorem prover).

But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).

And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)

While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.

I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).

That's a good point, although couldn't you usually black-box those and assume the invariants we expect of those primitives are in fact true? E.g. you don't need to bother trying to prove properties about your prng itself, you can just prove how your program behaves under a random oracle model.

If you're able to detect where you use these hard-to-analyse functions, then yes. This is feasible on source level, and maybe known compiler binary level. I think ultimately people will want to validate properties of binary code against the model specification of their hardware.

Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).

You can see that the blog post does not claim to solve the halting problem; instead, they pick a subset of behavior that is likely to be useful.

> You can see that the blog post does not claim to solve the halting problem;

Yes, true, they just ignored it and made unsupportable claims. And the Halting Problem cannot be "solved," that is what the Halting Problem says and proves.

No, the claims they made are well supported.

> No, the claims they made are well supported.

Here's the claim:

> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.

The claim "Find and patch all bugs" is false. This is computer science 101. It is not possible. All one can say is that the claims are well-repeated. They aren't supported at all.

If you were a little slower to jump to conclusions you might see that the blog post does not actually make the elementary blunder of not understanding how Rice's Theorem works, and that the claims made are qualified correctly as they come from people who are quite good at understanding what formal verification is and can do ;)

Reply on news.ycombinator.com