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

281–290 of 448 posts

Re: AI will make formal verification go mainstream

#281

Post by rixed »

kreetx wrote: post #256
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…

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

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

Re: AI will make formal verification go mainstream

#282

Post by lukan »

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 experience, the more information is encoded in the type system, the more effort is required to change code."

Have you seen large js codebases? Good luck changing anything in it, unless they are really, really well written, which is very rare. (My own js code is often a mess)

When you can change types on the fly somewhere hidden in code ... then this leads to the opposite of clarity for me. And so lots of effort required to change something in a proper way, that does not lead to more mess.

Re: AI will make formal verification go mainstream

#283

Post by dhruv3006 »

Almondsetat wrote: post #257
est wrote: post #227

Earlier quoted context omitted.

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good

Thats something I agree with.

I am right now working on an offline api client: https://voiden.md/. I wonder if this can be a feature.

Re: AI will make formal verification go mainstream

#284

Post by est »

Joker_vD wrote: post #258
est wrote: post #237

Earlier quoted context omitted.

> if the system verified to work, then it works no matter how API is shaped That's the case for one-off integrations, but the messy part always comes when system goal changes Let's say formal verification could help to avoid some anti-patterns.

> Let's say formal verification could help to avoid some anti-patterns. I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal veri…

> I'd still like to hear about the actual mechanism of this happening

I am not an expert on this, but the worst API I've seen is those with hidden states.

e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back.

And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)

Re: AI will make formal verification go mainstream

#285

Post by wolvesechoes »

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…

Soon a lot of people will go out of the way and try to convince you that Rust is most productive language, functions having longer signatures than their bodies is actually a virtue, and putting .clone(), Rc or Arc everywhere to avoid borrow-checker complaints makes Rust easier and faster to write than languages that doesn't force you to do so.

Of course it is a hyperbole, but sadly not that large.

Re: AI will make formal verification go mainstream

#286

Post by est »

Almondsetat wrote: post #257
est wrote: post #227

Earlier quoted context omitted.

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good

> It cannot tell you if the spec if good

I beg to differ, if a spec is hard to verify, then it's a bad sign.

Re: AI will make formal verification go mainstream

#287

Post by ogogmad »

StilesCrisis wrote: post #195
giancarlostoro wrote: post #176

Earlier quoted context omitted.

> especially when we currently use all kinds of frameworks and libraries that already abstract away implementation details. This is my issue with algorithm driven interviewing. Even the creator of Homebrew got denied by Google because he couldn't do some binary sort or whatever it even was. He made a tool used by millions of developers, but apparently that's not good enough.

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?

Re: AI will make formal verification go mainstream

#288

Post by hamiecod »

Davidzheng wrote: post #123
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…

OK but if the verification loop really makes the agents MUCH more useful, then this usefulness difference can be used as a training signal to improve the agents themselves. So this means the current capabilities levels are certainly not going to remain for very long (which is also what I expect but I would like to point out it's also supported by this)

Thats a strong RL technique that could equal the quality of RLHF.

Re: AI will make formal verification go mainstream

#289

Post by egwor »

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

I think that’s because the barrier to entry for a beginner is much higher than say python.

Re: AI will make formal verification go mainstream

#290

Post by atakan_gurkan »

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.

This sounds very interesting. Do you have a reference?
Post reply on HN