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

31–40 of 448 posts

Re: AI will make formal verification go mainstream

#31

Post by Wowfunhappy »

ManuelKiessling wrote: post #27
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…

Isn‘t it funny how that’s exactly the kind of stuff that helps a human developer be successful and productive, too? Or, to put it the other way round, what kind of tech leads would we be if we told our junior engineers „Well, here’s the codebase, that’s all I‘ll give you. No debuggers, linters, or test runners for you. Using a browser on your frontend implementation? Nice try buddy! Now good luck getting those requir…

> Isn‘t it funny how that’s exactly the kind of stuff that helps a human developer be successful and productive, too?

I think it's more nuanced than that. As a human, I can manually test code in ways an AI still can't. Sure, maybe it's better to have automated test suites, but I have other options too.

Re: AI will make formal verification go mainstream

#32

Post by pooooooooooooop »

yuppiemephisto wrote: post #22

I vibe code extremely extensively with Lean 4, enough to run out 2 claude code $200 accounts api limits every day for a week. I added LSP support for images to get better feedback loops and opus was able to debug https://github.com/alok/LeanPlot . The entire library was vibe coded by older ai. It also wrote https://github.com/alok/hexluthor (a hex color syntax highlighting extension that uses lean’s metaprogramming a…

cool quote about smooth operator ... I notice none of the vibe codes are proofs of anything and rather frameworks for using lean. this seems like a waste of tokens - what is your thinking behind this?

Re: AI will make formal verification go mainstream

#34

Post by bgwalter »

No it won't. People who aren't interested in writing specifications now won't be interested later as well. They want to hit the randomization button on their favorite "AI" jukebox.

If anyone does write a specification, the "AI" won't get even past the termination proof of a moderately complex function, which is the first step of accepting said function in the proof environment. Before you can even start the actual proof.

This article is pretty low on evidence, perhaps it is about getting funding by talking about "AI".

Re: AI will make formal verification go mainstream

#35

Post by heliumtera »

Will formal verification be a viable and profitable avenue for the middle man to exploit and fuck everybody else? Then yes, it absolutely will become mainstream. If not, them no, thanks. Everything that becomes mainstream for SURE will empower the middleman and cuck the developer, nothing else really matters. This is literally the only important factor.

Re: AI will make formal verification go mainstream

#37

Post by Uehreka »

101008 wrote: post #26
bglazer wrote: post #25

Earlier quoted context omitted.

This is a very tiring criticism. Yes, this is true. But, it's an implementation detail (tokenization) that has very little bearing on the practical utility of these tools. How often are you relying on LLM's to count letters in words?

It's an example that shows that if these models aren't trained in a specific problem, they may have a hard time solving it for you.

No, it’s an example that shows that LLMs still use a tokenizer, which is not an impediment for almost any task (even many where you would expect it to be, like searching a codebase for variants of a variable name in different cases).

Re: AI will make formal verification go mainstream

#38

Post by WhyOhWhyQ »

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…

I've tried getting claude to set up testing frameworks, but what ends up happening is it either creates canned tests, or it forgets about tests, or it outright lies about making tests. It's definitely helpful, but feels very far from a robust thing to rely on. If you're reviewing everything the AI does then it will probably work though.

Re: AI will make formal verification go mainstream

#39

Post by CobrastanJorji »

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…

I might go further and suggest that the key to getting useful results out of HUMAN coding agents is also to have good mechanisms in place to help them exercise and validate the code.

We valued automated tests and linters and fuzzers and documentation before AI, and that's because it serves the same purpose.

Post reply on HN