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

91–100 of 117 posts

Re: We have proof automation now

#91

Post by nickpsecurity »

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…

There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.

Re: We have proof automation now

#92

Post by vatsachak »

DavidSJ wrote: post #28
vatsachak wrote: post #22

Earlier quoted context omitted.

Worse than 0.01% of humans means that there are 8,000,000 people better than it. I know that's being pedantic I understand what you're saying. But every time I use Codex unless I specifically give it the abstractions it writes code that is way too specific.

> Worse than 0.01% of humans means that there are 8,000,000 people better than it. I know that's being pedantic I understand what you're saying. Since we're being pedantic, it means that there are (approximately) 800,000 people better than it. ;)

You're right, forgot a factor of 10 whoops

Re: We have proof automation now

#93

Post by [deleted] »

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…

[deleted]

Re: We have proof automation now

#94

Post by smj-edison »

prplfsh wrote: post #58
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…

It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.

Most math does proofs somewhat informally (as in the proofs are written in a conversational style, and they're considered valid when they convince the majority of mathemeticians), but those proofs can be traced back to ZFC (a specific formulation of set theory and first order logic).

Type theory, especially dependant types, are a pretty recent development, and aren't really used in practice in math. Even in Mathlib (what most people mean when they say they've used lean), they encode first order logic. The proofs are dependently typed, but the actual logic of the proof is all in ZFC.

Re: We have proof automation now

#95

Post by vatsachak »

rafaelRiv wrote: post #82
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

Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions

Re: We have proof automation now

#96

Post by nilkn »

boccaff wrote: post #47
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…

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.

Yes, this is a challenge, but I don't think it's as damning as it sounds.

First, the same kind of issue exists with any kind of testing. We all know that having unit tests and integration tests doesn't mean the software is correct and bug-free. Yet we still often believe it's worth investing in writing and maintaining a test suite. Formal methods is an additional level of assurance that I suspect we'd generally find worth it for critical software if it were easy enough to implement, even if it's not perfect.

Second, because formal verification has been so hard, nobody has really bothered making a serious attempt at solving the spec problem before (at least not to my knowledge). We've spent decades building frameworks that make writing tests really easy. We really have not come close to investing the same kind of effort into building frameworks and tools to make writing formal specs easy. I can imagine a world where we have sophisticated tools that help us create specs, plus real-time verification infrastructure that automatically reverifies code against the spec on each PR.

Third, and perhaps most importantly, there are many industries where this is actually low-hanging fruit: aerospace, medical devices, etc., actually already have formal specs that are verified manually by human engineers to satisfy certification requirements. I believe that's a more natural starting point vs. trying to scale formal methods for all software in general.

Re: We have proof automation now

#97

Post by makira »

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…

This is great! Not sure which high level language you are targetting, but consider Subrust instead of C:

https://github.com/orbitalhigh/subrust

How does LowIRSSA compare to P1pp from boot2 ?

Re: We have proof automation now

#98

Post by andrewla »

jason_s wrote: post #26

OK so this article is sort of about formal proof automation, but it seems more practically about Zstandard, which I very much enjoyed reading.

Yeah, this is really cool. I'm now deep in the rabbit hole of FSE encoding and ANS & tANS. The last time I poked my head in here, range encoding and arithmetic encoding were the state of the art for fractional entropy representations, but they both sucked. This is a million times better and so simple that I feel like I should have invented it myself.

Re: We have proof automation now

#99

Post by jerf »

boccaff wrote: post #47
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…

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.

Just as an addendum to some of the other fine replies you've got, one of the things I'm interested in for formal verification is security assertions, and those don't necessarily need lots of comprehension to apply. If you can assert "this code never hits the network again" or "this code will never execute arbitrary code", the proof of that may be nontrivial but the comprehension of it is easy.

Proving that some complicated algorithm is actually what you think it is, even after you've proved that it does whatever it is it does, is hard. But to me, and me personally so not necessarily what everyone else thinks, that's not really what I'm interested in from proofs. I'm really more interested in these overarching declarations of what the code definitely doesn't do, or putting bounds on what it does, rather than proving that my billing code bills the customers precisely in the way I expect, when, frankly, the best specification of it I have is already what is in the unproved code base anyhow. I believe those have a very sensible story as to how both humans and AIs can use those assertions.

Re: We have proof automation now

#100

Post by rafaelRiv »

vatsachak wrote: post #95
rafaelRiv wrote: post #82

Earlier quoted context omitted.

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

Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions

I do but I have no guarantee that the llms will make a sane implementation of the types
Post reply on HN