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

81–90 of 117 posts

Re: We have proof automation now

#81

Post by yorwba »

el_pollo_diablo wrote: post #77
yorwba wrote: post #73

Earlier quoted context omitted.

> 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 r…

You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.

Re: We have proof automation now

#82

Post by rafaelRiv »

colechristensen wrote: post #62

I think people are overestimating the usefulness LLMs will bring us based on early examples of low hanging fruit being harvested. LLMs have a VERY different set of things which are easy and which are hard and from software security to math proofs we're seeing very early impressive results but those will run out and new classes of what is difficult will show themselves. The "this new tech will cause everything to be e…

I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet

Re: We have proof automation now

#83

Post by el_pollo_diablo »

less_less wrote: post #75
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…

In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical properties as the value is moved around. That is why I mentioned them in the context of opaque types. This is especially useful with generics: when a type parameter is instantiated with a dependent type, all its occurrences instantly benefit from the strong typing.

They can also be used to enforce just enough constraints on the inputs of a function to make it total, but this comes down to the tradeoff between either leaving an error path in the program and proving its unreachability later, or not having this error path but immediately requiring the proof. In any case, as you mention, further properties can be proved later without altering the dependent type.

I do not intend to come off as overly negative about dependent types. They have their uses, but they can also bring a maintenance nightmare.

Re: We have proof automation now

#84

Post by el_pollo_diablo »

yorwba wrote: post #81
el_pollo_diablo wrote: post #77

Earlier quoted context omitted.

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 r…

You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.

> a single proof covering the most precise description of the program's behavior is more compact

Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form.

Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proof assistants that largely reduce the length of proof scripts. This is mostly a matter of tooling.

Re: We have proof automation now

#85

Post by justincormack »

andai wrote: post #66

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was…

re "An LLM also pointed that out, so I guess it must have been a different one which implemented it?" - no, there is no correlation between whether the same LLM is used and whether it can find errors.

Re: We have proof automation now

#86

Post by yorwba »

el_pollo_diablo wrote: post #84
yorwba wrote: post #81

Earlier quoted context omitted.

You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.

> a single proof covering the most precise description of the program's behavior is more compact Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form. Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proo…

Yes, if you don't mind the repetition or have tooling to deal with it, you can have multiple separate proofs, dependent types won't stop you.

Re: We have proof automation now

#88

Post by m1el »

logicchains wrote: post #44
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…

Have you heard of https://cakeml.org/ ? It's a self-hosting formally verified compiler.

Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties.

Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...

Re: We have proof automation now

#89

Post by im3w1l »

hajile wrote: post #67
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…

You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords. Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true bec…

I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually:

    * Understandable
    * Portable across projects, you could imagine something like
        from specs import no_stealing_secrets
        no_stealing_secrets(secret_table)
    * Implicitly proves the absence of RCE, though I suppose
        it could allow something truly crazy like an interpreter
        that will run any attacker supplied program that can 
        be proven not to steal the specified secrets

Re: We have proof automation now

#90

Post by m1el »

hajile wrote: post #67
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…

You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords. Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true bec…

I understand that formal verification is not panacea.

My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".

We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.

Post reply on HN