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

401–410 of 448 posts

Re: AI will make formal verification go mainstream

#401

Post by giancarlostoro »

9rx wrote: post #356
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 ?

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…

> Same as why companies in the past used to reject anyone without a degree.

They still do, and its a shame some of the smartest most capable developers I know have no degree.

Re: AI will make formal verification go mainstream

#402

Post by kazinator »

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.

Programs are not limited; the number of Turing machines is countably infinite.

When you say things like "eliminate a class of bugs", that is played out in the abstraction: an infinite subset of that infinity of machines is eliminated, leaving an infinity.

How you then sample from that infinity in order to have something which fits on your actual machine is a separate question.

Re: AI will make formal verification go mainstream

#403

Post by marcosdumay »

Maxion wrote: post #338
marcosdumay wrote: post #113

Earlier quoted context omitted.

There are many really important properties to enforce even on the most basic CRUD system. You can easily say things like "an anonymous user must never edit any data, except for the create account form", or "every user authorized to see a page must be listed on the admin page that lists what users can see a page". People don't verify those because it's hard, not for lack of value.

Even > "an anonymous user must never edit any data, except for the create account form" Can quickly end up being > "an anonymous user must never edit any data, except for the create account form, and the feedback form" And a week later go to > "an anonymous user must never edit any data, except for the create account form, the feedback form, and the error submission form if they end up with a specific type of error"…

It is still a small rule, with plenty of value. It's nowhere near the size of the access control for the entire site. And it's also not written down by construction.

It changing with time doesn't make any of that change.

Re: AI will make formal verification go mainstream

#404

Post by apitman »

simonw wrote: post #2

I'm convinced now that the key to getting useful results out of coding agents (Claude Code, Codex CLI etc) is having good mechanisms in place to help those agents exercise and validate the code they are writing. At the most basic level this means making sure they can run commands to execute the code - easiest with languages like Python, with HTML+JavaScript you need to remind them that Playwright exists and they shou…

That's bad news for C++, Rust, and other slow compilers.

Re: AI will make formal verification go mainstream

#405

Post by apitman »

astrostl wrote: post #169
roadside_picnic wrote: post #62

Earlier quoted context omitted.

I very much agree, and believe using languages with powerful types systems could be a big step in this direction. Most people's first experience with Haskell is "wow this is hard to write a program in, but when I do get it to compile, it works". If this works for human developers, it should also work for LLMs (especially if the human doesn't have to worry about the 'hard to write a program' part). > The next step up…

This is why I use Go as much as reasonably possible with vibe coding: types, plus great quality-checking ecosystem, plus adequate training data, plus great distribution story. Even when something has stuff like JS and Python SDKs, I tend to skip them and go straight to the API with Go.

Also a fast compiler which lets the agent iterate more times.

Re: AI will make formal verification go mainstream

#406

Post by pron »

avmich wrote: post #242
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…

Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.

Writing in a language that guarantees termination is not very interesting in itself, as every existing program could automatically be translated into a non-Turing-complete language where the program is proven to terminate, yet behaves exactly the same: the language is the same as the original, only loops/rectursion ends the program after, say, 2^64 iterations. This, in itself, does not make programs any easier to analyse. In fact, a language that only has boolean variables, no arrays, no recursion, and loops of depth 2 at most is already instractable to verify. It is true that programs in Turing-complete languages cannot generally be verified in efficiently, but most non-Turing-complete languages also have this property.

Usually, when we're interested in termination proofs, what we're really interested in is a proof that the algorithm makes constant progress that converges on a solution.

Re: AI will make formal verification go mainstream

#407

Post by fsloth »

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…

"decide what the software is supposed to do in the first place."

After 20 years of software development I think that is because most of the software out there, is the method itself of finding out what it's supposed to do.

The incomplete specs are not lacking feature requirements due to lack of discipline. It's because nobody can even know without trying it out what the software should be.

I mean of course there is a subset of all software that can be specified before hand - but a lot of it is not.

Knuth could be that forward thinking with TeX for example only because he had 500 years of book printing tradition to fall back on to backport the specs to math.

Re: AI will make formal verification go mainstream

#408

Post by Hercuros »

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.

How do you count how many bugs a program has? If I replace the Clang code base by a program that always outputs a binary that prints hello world, how many bugs is that? Or if I replace it with a program that exits immediately?

Maybe another example is compiler optimisations: if we say that an optimising compiler is correct if it outputs the most efficient (in number of executed CPU instructions) output program for the every input program, then every optimising compiler is buggy. You can always make it less buggy by making more of the outputs correct, but you can never satisfy the specification on ALL inputs because of undecidability.

Re: AI will make formal verification go mainstream

#409

Post by hwayne »

pron wrote: post #351
hwayne wrote: post #178

Earlier quoted context omitted.

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

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.

Re: AI will make formal verification go mainstream

#410

Post by TimTheTinker »

jandrese wrote: post #388
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…

The danger of this is people start asking about formally verified specs, and down that road lies madness. "If you can formally verify the spec the code can be auto-generated from it."

Most formal "specs" (the part that defines the system's actual behavior) are just code. So a formally verified (or compiled) spec is really just a different programming language, or something layered on top of existing code. Like TypeScript types are a non-formal but empirical verification layer on top of JavaScript.

The hard part remains: translating from human-communicated requirements to a maintainable spec (formally verified or not) that completely defines the module's behavior.

Post reply on HN