Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

We have proof automation now

imperialviolet.org

Post reply on HN
Print view View original

71–80 of 117 posts

Re: We have proof automation now

#71

Post by eru »

andor wrote: post #56
boccaff wrote: post #47

Earlier quoted context omitted.

Don't we still need to verify that what the LLM proved is actually the stated system?If agents cutting corners (like deleting tests) is a concern, how can we be sure that the verification corresponds to the software and that every _load bearing_ assumption is true? I don't think that simply trusting the Lean core is enough.

The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system. You still need to verify that the generated code is what you asked for, though.

> The LLM does not prove anything (it cannot reason).

What is that supposed to mean?

> It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system.

Yes, and that's great. (Though, of course, the computer doesn't execute lean directly, it gets translated first.)

> You still need to verify that the generated code is what you asked for, though.

Yes, but you only need to read the theorems, not the proofs nor code.

Re: We have proof automation now

#72

Post by thaumasiotes »

m1el wrote: post #27

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vul…

> We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point)

But... if that's not the point, the claim is obviously untrue. The security industry includes public-facing bug bounty platforms. Those find far more vulnerabilities than Mythos ever will, if you're not even worried about what counts as a vulnerability.

Re: We have proof automation now

#73

Post by yorwba »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

> you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.

Having to do this is a sign that the new property depends on implementation details in some way. This can definitely feel like annoying busywork when there is only one reasonable implementation. Of course your sorting algorithm doesn't change the multiplicity of elements in the array, you wouldn't write a bug like that. Of course your sorting algorithm doesn't change the order of elements that are already sorted correctly, you wouldn't write a bug like... except unstable sorting algorithms do that and are widely used for performance reasons. So you do have to check your actual implementation step by step to verify that it really does what you think it must of course be doing. Trying to separate the concerns does not change this.

Re: We have proof automation now

#74

Post by saithound »

codebje wrote: post #7
nextos wrote: post #3

I agree with the core thesis that LLMs + theorem provers might make formal methods cheap enough to be practical in software development. The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent. From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite ea…

IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should d…

> . You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. [..] it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.

Indeed. The last bug I fixed in a production app was one where people could not restore from backup due to a de/serialization issue. The correct behavior would have been straightforward to specify (round-tripping). Trying to verify the serializer against the correct behavior would have forced the devs to think through all the edge cases.

Re: We have proof automation now

#75

Post by less_less »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

I agree to some extent with your thesis. But also you don't have to encode all the properties of the program in dependent types everywhere. You can have the implementation contain either no proofs or fairly few (e.g., termination and no UB, which can often be automatically discharged), and then separately prove things about it. E.g.

    def function_spec bleh blah := math_blargh
    def function_impl bleh blah := code_blargh
    theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }
or whatever. That way the function's spec and implementation remain separate and readable. In my limited experience, Lean code usually works more this way rather than having the whole function and its spec in a giant dependently-typed object. For imperative code you can also use Hoare triples and vcgen, but that's currently only partly baked (i.e. proving things is a giant pain).

Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.

Re: We have proof automation now

#76

Post by rafaelRiv »

el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

I would say that the value of dependent types in software engineering isn't in proving all code correctness. As a user pointed out in the idris2 Zulip, most programs using dependent types don't have, and shouldn't have, proof of validity for the entire program. Instead, you simply get more correct code by construction, and I think that's the whole point.

I'm currently developing a unikernel in idris2, and the experience is very pleasant (unfortunately, I'm not quite ready to share it yet).

Re: We have proof automation now

#77

Post by el_pollo_diablo »

yorwba wrote: post #73
el_pollo_diablo wrote: post #45

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, wit…

> you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program. Having to do this is a sign that the new property depends on implementation details in some way. This can definitely feel like annoying busywork when there is only one reasonable implementation. Of course your sorting algorithm doesn'…

I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.

For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved

    {P∧B}S{P}
and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove

    {Q∧B}S{Q}
or even

    {P∧Q∧B}S{Q}
if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove

    {P∧Q∧B}S{P∧Q}
which is incomparable and uselessly mixes both concerns.

Re: We have proof automation now

#78

Post by vessenes »

I think it's worth putting a Knuth quote up on your board when you think about verification as an end goal: "Beware of bugs in the above code; I have only proved it correct, not tried it."

Or, as Wolfram proposes in another link on the front page today, the irreducibility of computation means we cannot generally get all bugs out of systems.

To my mind, one of the risks of going all in on verification is that you just move the difficulty to a harder, more abstract layer - the specification. In my experience, this typically looks appealing to a 'type' -- very high IQ, very little real world engineering experience -- it's a dream that hits the inevitable grittiness of the real world and .. the real world keeps winning.

Re: We have proof automation now

#79

Post by empath75 »

m1el wrote: post #27

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vul…

I had claude spend about 2 hours friday modeling one of our kubernetes operators in TLA, and it found 8 bugs, including 2 that could cause data loss, and one of the other bugs was one we had been trying to figure out why it was happening for literally months.

Re: We have proof automation now

#80

Post by empath75 »

gz09 wrote: post #13

Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done. Verus ( https://github.com/verus-lang/verus ) i…

I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally verify a Rust-like borrow checker and at this point I have a working interpreter and LLVM compiler and a formally verified kernel.

All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.

Post reply on HN