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

AI will make formal verification go mainstream

martin.kleppmann.com

Post reply on HN
Print view View original

441–448 of 448 posts

Re: AI will make formal verification go mainstream

#441

Post by pron »

pron wrote: post #415
hwayne wrote: post #409

Earlier quoted context omitted.

Those things, unlike floats, have approximable-enough facsimiles that you can verify instead. No tools support even fixed point decimals. This has burned me before when I e.g needed to take the mean of a sequence.

You say no tools but you can "verify floats" with TLAPS. I don't think that RAM or 64-bit integers have facsimiles in TLA+. They can be described mathematically in TLA+ to whatever level of detail you're interested in (e.g. you have to be pretty detailed when describing RAM when specifying a GC, and even more when specifying a CPU's memory-access subsystem), but so can floating point numbers. The least detailed descr…

P.S. for the case of computing a mean, I would use Real rather than try to model floating point if the idiosyncracies of a particular FP implementation were important. That means you can't use TLC. In some situations it could suffice to represent the mean as any number (even an integer) that is ≥ min and ≤ max, but TLC isn't very effective even for algorithms involving non-tiny sets of integers when there's "interesting" arithmetic involved.

I don't know the state of contemporary model checkers that work with theories of reals and/or FP, and I'm sure you're much more familar with that than me, but I believe that when it comes to numeric computation, deductive proofs or "sampling tests" (such as property-based testing) are still more common than model-checking. It could be interesting to add a random sampling mode to TLC that could simulate many operations on reals using BigDecimal internally.

Re: AI will make formal verification go mainstream

#442

Post by suspended_state »

AlienRobot wrote: post #430
suspended_state wrote: post #390

Earlier quoted context omitted.

> A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way. That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language. Edit: I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as…

>an error of translation from natural language to formal language Really? Programming languages are all formal languages, which means all human-made errors in algorithms wouldn't be "bugs" anymore. Some projects even categorize typos as bugs, so that's a unusually strict definition of "bug" in my opinion.

Sure, I guess you can understand what I said that way, but that's not what I meant. I wasn't thinking about the implementation, but the specifications.

Read again the quote I was refering to if you need better context to understand my comment.

If you have good formal specifications, you should be able to produce the corresponding code. Any error in that phase should be considered a bug, and yes, a typo should fit that category, if it makes the code deviate from the specs.

But an error in the step of translating the requirements (usually explained in natural language) to specifications (usually described formally) isn't a bug, it's a translation error.

Re: AI will make formal verification go mainstream

#443

Post by justatdotin »

CyberDildonics wrote: post #394
justatdotin wrote: post #202

Earlier quoted context omitted.

my experience is that llm programming and rust can fit together very nicely, thankyou. I am finding agent tooling expands my capacity for multi-language projects

This seems like it's intentional at this point. Try to follow me. The whole point is that if someone needs to lean on LLMs in the first place and they have problems with the language, they go to a different language instead of stopping using LLMs.

I think I do understand your claim,

which is why I am offering my personal experience as counter-evidence.

agents can empower us to choose the best language for the job, rather than defaulting to one which we are most familiar with.

I suspect our difference in opinion comes from your attitude about tools as a crutch to lean on vs a lever to apply.

Re: AI will make formal verification go mainstream

#444

Post by CyberDildonics »

justatdotin wrote: post #443
CyberDildonics wrote: post #394

Earlier quoted context omitted.

This seems like it's intentional at this point. Try to follow me. The whole point is that if someone needs to lean on LLMs in the first place and they have problems with the language, they go to a different language instead of stopping using LLMs.

I think I do understand your claim, which is why I am offering my personal experience as counter-evidence. agents can empower us to choose the best language for the job, rather than defaulting to one which we are most familiar with. I suspect our difference in opinion comes from your attitude about tools as a crutch to lean on vs a lever to apply.

There isn't a difference of opinion you aren't replying to what I'm saying in the first place.

Re: AI will make formal verification go mainstream

#445

Post by int_19h »

rixed wrote: post #281
kreetx wrote: post #256

Earlier quoted context omitted.

Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.

And one can see how quickly they became mainstream...

Given that it's the AI doing the coding, it would be pretty quickly so long as it's decent at Haskell. Which it already is, surprisingly so actually for such a niche language. It doesn't necessarily write great code, but it's good enough, and the straightjacket type system makes it very hard for the model to sneak in creative hacks like using globals, or trip itself with mutable state.

Re: AI will make formal verification go mainstream

#446

Post by rocqua »

nomadygnt wrote: post #217
rocqua wrote: post #11

I've been trying to convince others of this, and gotten very little traction. One interesting response I got from someone very familiar with the Tamarin prover was that there just wasn't enough example code out there. Another take is that LLMs don't have enough conceptual understanding to actually create proofs for the correctness of code. Personally I believe this kind of work is predicated on more ergonomic proof s…

Another cool tool that’s being developed for rust is verus. It’s not the same as Kani and is more of a fork of the rust compiler but it lets you do some cool verification proofs combined with the z3 SMT solver. It’s really a cool system for verified programs.

I had a look, and it seems cool. But it doesn't seem to do the thing I love about Kani: work with only very partial annotations, only proving the annotations and being a very light lift on code not relevant for the annotations.

Re: AI will make formal verification go mainstream

#447

Post by pron »

igornotarobot wrote: post #328
nyrikki wrote: post #121

Earlier quoted context omitted.

TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Us…

> TLA+ is not a silver bullet, and like all temporal logic, has constraints. > > You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” I think people get confused by the word "temporal" in the name of TLA+. Yes, it has temporal operators. If you throw them away, TLA+ (minus the temporal operators) would be still extremely useful f…

The "temporal" in TLA+ isn't about □ and ⬦. It's about ' and the abstraction-refinment relation with stuttering at its core (contrasted with o and its non-stuttering meaning). Of course, you can't really specify anything in TLA+ without □ (unless you rely on TLC, which inserts the □ for you).

You cannot specify much in TLA+ without ' and □, andtThe "temporal" part of TLA+ - i.e. the TLA logic - is essential; but saying it's like "all temporal logics" is ignoring the abstraction-refinement relation, which is the heart of TLA+ (that's what ⇒, basic implication, in TLA+ means) and other temporal logics miss.

Of course, you could hypothetically use the + part of TLA+, the formalised set theory, to specify everything, but that would be very inconvenient.

Re: AI will make formal verification go mainstream

#448

Post by pron »

DoctorOetker wrote: post #419
pron wrote: post #99

Earlier quoted context omitted.

I completely agree it's appealing, I just don't see a reason to assume that an agent will be able to succeed at it and at the same time fail at other things that could make the whole exercise redundant. In other words, I also want agents to be able to consistently prove software correct, but if they're actually able to accomplish that, then they could just as likely be able to do everything else in the production of…

>I just don't see a reason to assume that an agent will be able to succeed at it and at the same time fail at other things that could make the whole exercise redundant. But that is much simpler to understand: eventually finding a proof using guided search (machines searching for proofs, multiple inference attempts) takes more effort than verifying a proof. Formal verification does not disappear, because communicating…

> eventually finding a proof using guided search (machines searching for proofs, multiple inference attempts) takes more effort than verifying a proof. Formal verification does not disappear, because communicating a valuable succinct proof is much cheaper than having to search for the proof anew. The proofs will become inevitable lingua franca (like it is among capable humans) for computers as well. Basic economics will result in adoption of formal verification.

But AI isn't used to verify the proof. It's used to find it. And if it can find it - one of the hardest things in software development - there's no reason to believe it can't do anything else associated with software development. If AI agents find formal verification helpful, they would probably opt to use it, but there would also be no need for a human in the loop at all.

> It is currently already much better than the average human at finding proofs.

The average human also can't write hello world. LLMs are currently significantly worse at finding proofs than the average formal-verification person (I say this as someone who's done formal verification for many years), though, just as they're significantly worse at writing code than the average programmer. I'm not saying they won't become better, it's just strange to expect that they'll become better than the average formal-verification person and at the same time they won't be better than the average product manager.

> there will always be problems it can not instantly generate provably correct software

Nobody said anything about "instantly". If the AI finds formal verification helpful, it will choose to use it, but if it can find proofs better than humans, why expect that it won't be able to do easier tasks better than humans?

Post reply on HN