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

391–400 of 448 posts

Re: AI will make formal verification go mainstream

#391

Post by anovick »

alexgotoi wrote: post #373

The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…

OP seems not broadly applicative to corporate software development.

Rather, it's directed at the kind of niche, mission-critical things, that not all of which are getting the formal verification solution that is needed for them and/or that don't get considered due to high costs (due to specialization skill).

I read OP as a realization that the costs have fallen, and thus we should see formal verification more than before.

Re: AI will make formal verification go mainstream

#392

Post by gls2ro »

suspended_state wrote: post #390
TimTheTinker wrote: post #377

Earlier quoted context omitted.

> it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. Not only that, but it's been well-established that a significant challenge with formally verified software is to create the right spec -- i.e. one that actually satisfies the intended requirements. A formally verified program can still have bugs, because the spec (which requires specialized sk…

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

In some definitions (that I happen to agree with but because we wanted to save money by first not properly training testers and then getting rid of them is not present so much in public discourse) the purpose of testing (or better said quality control) is:

1) Verify requirements => this can be done with formal verifications

2) Validate fit for purpose => this is where we make sure that if the customer needs addition it does not matter if our software does very well substraction and it has a valid proof of doing that according with specs.

I know this second part is kinda lost in the transition from oh my god waterfall is bad to yeyy now we can fire all testers because the quality is the responsibility of the entire team.

Re: AI will make formal verification go mainstream

#393

Post by gls2ro »

tmtvl wrote: post #386
kazinator wrote: post #324

Earlier quoted context omitted.

If you eliminate the odd integers from consideration, you've eliminated an entire class of integers. yet, the set of remaining integers is of the same size as the original.

There cannot be infinite bugs in a limited program.

Because the number of state where a program can be is so huge (when you consider everything that can influence how a program runs and the context where and when it runs) it is for the current computation power practically infinite but yes it is theoretically finite and can even be calculated.

Re: AI will make formal verification go mainstream

#394

Post by CyberDildonics »

justatdotin wrote: post #202
CyberDildonics wrote: post #200

Earlier quoted context omitted.

You're missing the point of what I said. If LLM programming and rust conflict people don't suddenly learn to program and stay with rust, they find a new language.

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.

Re: AI will make formal verification go mainstream

#396

Post by skydhash »

nwah1 wrote: post #384
QuadrupleA wrote: post #203

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…

> Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server) Isn't this what TLA+ was meant to deal with?

Not really, some components like components have a lot of properties that’s very difficult to modelize. Take latency in network, or storage performance in OS.

Re: AI will make formal verification go mainstream

#397

Post by riku_iki »

infruset wrote: post #134

I was waiting for a post like this to hit the front page of Hacker News any day. Ever since Opus 4.5 and GPT 5.2 came out (mere weeks ago), I've been writing tens of thousands of lines of Lean 4 in a software engineering job and I feel like we are on the eve of a revolution. What used to take me 6 months of work when I was doing my PhD in Coq (now Rocq), now takes from a few hours to a few days. Whole programming lan…

> I've been writing tens of thousands of lines of Lean 4 in a software engineering job

I am wondering what exactly you are doing? What tasks you are solving using generated lean?

Re: AI will make formal verification go mainstream

#398

Post by dwrodri »

I think if AI can help us modernize the current state of hardware verification, I think that would be an enormous boon to the tech industry.

Server class CPUs and GPUs are littered with side channels which are very difficult to “close”, even in hardened cloud VMs.

We haven’t verified “frontier performance” hardware down to the logic gate in quite some time. Prof. Margaret Martinosi’s lab and her students have spent quite some time on this challenge, and i am excited to see better, safer memory models oyt in the wild.

A lot of the same big ideas used in hardware are making their way into the software later too, see https://faultlore.com/blah/tower-of-weakenings/

Re: AI will make formal verification go mainstream

#399

Post by iamwil »

I wrote a post on how I dipped my toes into Lean, using LLMs to guide me.

https://interjectedfuture.com/the-best-way-to-learn-might-be...

You might find it useful. I also caveat the experience and recount some of the pitfalls, which you might enjoy as a skeptic.

Martin Klepmann seemed to like it too. https://bsky.app/profile/martin.kleppmann.com/post/3m7ugznx4...

Re: AI will make formal verification go mainstream

#400

Post by giancarlostoro »

ogogmad wrote: post #354
giancarlostoro wrote: post #310

Earlier quoted context omitted.

They certainly don't filter out toxic people who make others leave companies because they poison the well.

I have a suspicion that "good candidate" is being gerrymandered. What might have been "good" in 1990 might have become irrelevant in 2000+ or perhaps detrimental. I say that as someone who is actually good at algorithm questions himself. I think GP, as well as other Google defenders, are parroting pseudo-science.

I agree. But also if it works to get you jobs there, why wouldn't you defend it? I mean I might be inclined to do so as well, it guarantees me a place even if I lack soft skills for the role.
Post reply on HN