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

351–360 of 448 posts

Re: AI will make formal verification go mainstream

#351

Post by pron »

hwayne wrote: post #178
pron wrote: post #174

Earlier quoted context omitted.

> 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” You really don't. It's not LTL. Abstraction/refinement relations are at the core of TLA. > Or even floats [0] and it becomes challenging and strings are a mess. No problem with floats or strings as far as specification goes. The particular verification tools you choose to run…

> No problem with floats or strings as far as specification goes. The particular verification tools you choose to run on your TLA+ spec may or may not have limitations in these areas, though. I think it's disingenuous to say that TLA+ verifiers "may or may not have limitations" wrt floats when none of the available tools support floats. People should know going in that they won't be able to verify specs with floats!

I'm not sure how a "spec with floats" differs from a spec with networks, RAM, 64-bit integers, multi-level cache, or any computing concept, none of which exists as a primitive in mathematics. A floating point number is a pair of integers, or sometimes we think about it as a real number plus some error, and TLAPS can check theorems about specifications that describe floating-point operations.

Of course, things can become more involved if you want to account for overflow, but overflow can get complicated even with integers.

Re: AI will make formal verification go mainstream

#352

Post by GTP »

skissane wrote: post #296
gizmo686 wrote: post #211

Earlier quoted context omitted.

A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…

> For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it. The problem is there is always some chance a coding agent will g…

With the added issue that now the expert is working with code they didn't write, and that could be in general be harder to understand than human-written code. So they could find it easier to just throw it away and start from scratch.

Re: AI will make formal verification go mainstream

#353

Post by GTP »

blub wrote: post #270
gizmo686 wrote: post #211

Earlier quoted context omitted.

A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…

> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…

In my opinion, programming languages with a loose type system or no explicit type system only appear to foster productivity, because it is way easier to end up with undetected mistakes that can bite later, sometimes much later. Maybe some people argue that then it is someone else's problem, but even in that case we can agree that the overall quality suffers.

Re: AI will make formal verification go mainstream

#354

Post by ogogmad »

giancarlostoro wrote: post #310
ogogmad wrote: post #287

Earlier quoted context omitted.

I've heard this before. Why do you think algorithm questions are effective for finding "good" hires? Are they ?

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.

Re: AI will make formal verification go mainstream

#355

Post by igornotarobot »

It probably will, but not the way we all imagine. What we see now is an attempt to recycle the interactive provers that took decades to develop. Writing code, experimenting with new ideas and getting feedback has always been a very slow process in academia. Getting accepted at a top peer-reviewed conference takes months and even years. The essential knowledge is hidden inside big corps that only promote their "products" and rarely give the knowledge back.

LLMs enable code bootstrapping and experimentation faster not only for the vibe coders, but also for the researchers, many of them are not really good coders, btw. It may well be that we will see new wild verification tools soon that come as a result of quick iteration with LLMs.

For example, I recently wrote an experimental distributed bug finder for TLA+ with Claude in about three weeks. A couple of years ago that effort would require three months and a team of three people.

Re: AI will make formal verification go mainstream

#356

Post by 9rx »

ogogmad wrote: post #287
StilesCrisis wrote: post #195

Earlier quoted context omitted.

Google denies qualified people all the time. They would much rather reject a great hire than take a risk on accepting a mediocre one. I feel for him but it's just the nature of the beast. Not everyone will get in.

I've heard this before. Why do you think algorithm questions are effective for finding "good" hires? Are they ?

The intent isn't to find good hires per se, but to whittle down the list of applicants to a manageable number in a way that doesn't invite discrimination lawsuits.

Same as why companies in the past used to reject anyone without a degree. But then everyone got a degree, leaving it to no longer be an effective filter, hence things like algorithm tests showing up to fill the void.

Once you've narrowed the list, then you can worry about figuring out who is "good" through giving the remaining individuals additional attention.

Re: AI will make formal verification go mainstream

#357

Post by pron »

mrkeen wrote: post #240
pron wrote: post #90

Earlier quoted context omitted.

> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many…

Can TLA+ prove anything about something you specify but don't execute?

You can write proofs in TLA+ about things you don't exectute and have them checked by the TLA+ proof assistant. But the most common aspect of that, which pretty much every TLA+ spec contains is nondeterminism, which is basically the ability to describe a system with details you don't know or care about. For example, you can describe "a program that sorts an array" without specifying how and then prove, say, that the median value ends up in the middle. The ability to specify what a program or a subroutine does without specifying how is what separates the expressive power of specification from programming. This extends not only to the program itself but to its environment. For example, it's very common in TLA+ to specify a network that can drop or reorder messages nondeterministically, and then prove that the system doesn't lose data despite that.

Re: AI will make formal verification go mainstream

#358

Post by pron »

pron wrote: post #51

> it’s not hard to extrapolate and imagine that process becoming fully automated in the next few years. And when that happens, it will totally change the economics of formal verification. There is a problem with this argument similar to one made about imagining the future possibilities of vibe coding [1]: once we imagine AI to do this task, i.e. automatically prove software correct, we can just as easily imagine it t…

To make this more constructive, I think that today AI tools are useful when they do things you already know how to do and can assess the quality of the output. So if you know how to read and write a formal specification, LLMs can already help translating natural-language descriptions to a formal spec.

It's also possible that LLMs can, by themselves, prove the correctness of some small subroutines, and produce a formal proof that you can check in a proof checker, provided you can at least read and understand the statement of the proposition.

This can certainly make formal verification easier, but not necessarily more mainstream.

But once we extrapolate the existing abilities to something that can reliably verify real large or medium-sized programs for a human who cannot read and understand the propositions (and the necessary simplifying assumptions) that it's hard to see a machine do that and at the same time not able to do everything else.

Re: AI will make formal verification go mainstream

#360

Post by jappgar »

teiferer wrote: post #277
blub wrote: post #270

Earlier quoted context omitted.

> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…

> In my experience, the more information is encoded in the type system, the more effort is required to change code. I would tend to disagree. All that information encoded in the type system makes explicit what is needed in any case and is otherwise only carried informally in peoples' heads by convention. Maybe in some poorly updated doc or code comment where nobody finds it. Making it explicit and compiler-enforced i…

It is definitely harder to refactor Haskell than it is Typescript. Both are "safe" but one is slightly safer, and much harder to work with.
Post reply on HN