Live data from Hacker News

AI will make formal verification go mainstream

martin.kleppmann.com

41–50 of 448 posts

Re: AI will make formal verification go mainstream

#41
post #25

GPT 5.2 can't even tell me how many rs are in garlic.

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?

At this point if I was openAI I wouldn’t bother fixing this to give pedants something to get excited about.

Re: AI will make formal verification go mainstream

#42
post #25

GPT 5.2 can't even tell me how many rs are in garlic.

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?

The criticism would stop if the implementation issue was fixed.

It's an example of a simple task. How often are you relying on LLMs to complete simple tasks?

Re: AI will make formal verification go mainstream

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

[deleted]

Re: AI will make formal verification go mainstream

#44
post #33

I've been toying with vibecoding rust - hardly formal verification, but it is a step closer than python that's for sure. So far so good, though the smaller amount of training data is noticeable.

vibecoding rust sounds cool, which model are you using? I have tried in the past with GPT4o and Sonnet 4, but they were so bad I thought I should just wait a few years.

Re: AI will make formal verification go mainstream

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

Where they'd get training data?

Source code generation is possible due to large training set and effort put into reinforcing better outcomes.

I suspect debugging is not that straightforward to LLM'ize.

It's a non-sequential interaction - when something happens, it's not necessarily caused the problem, timeline may be shuffled. LLM would need tons of examples where something happens in debugger or logs and associate it with another abstraction.

I was debugging something in gdb recently and it was a pretty challenging bug. Out of interest I tried chatgpt, and it was hopeless - try this, add this print etc. That's not how you debug multi-threaded and async code. When I found the root cause, I was analyzing how I did it and where did I learn that specific combination of techniques, each individually well documented, but never in combination - it was learning from other people and my own experience.

Re: AI will make formal verification go mainstream

#46

I love HN because HN comments have talked about this a fair bit already. I think on the recent Erdos problem submission. I like the idea that languages even like Rust and Haskell may be more accessible. Learn them of course but LLM can steer you out of getting stuck.

The idea that LLMs are steering anything correctly with Rust reference management is hilarious to me, but only due to my experiences.

Re: AI will make formal verification go mainstream

#47
post #45
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…

Where they'd get training data? Source code generation is possible due to large training set and effort put into reinforcing better outcomes. I suspect debugging is not that straightforward to LLM'ize. It's a non-sequential interaction - when something happens, it's not necessarily caused the problem, timeline may be shuffled. LLM would need tons of examples where something happens in debugger or logs and associate i…

How long ago was this? I've had outstansingly impressive results asking Copilot Chat with Sonnet 4.5 or ChatGPT to debug difficult multithreaded C++.

Re: AI will make formal verification go mainstream

#48
post #45
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…

Where they'd get training data? Source code generation is possible due to large training set and effort put into reinforcing better outcomes. I suspect debugging is not that straightforward to LLM'ize. It's a non-sequential interaction - when something happens, it's not necessarily caused the problem, timeline may be shuffled. LLM would need tons of examples where something happens in debugger or logs and associate i…

Have you tried running gdb from a Claude Code or Codex CLI session?

Re: AI will make formal verification go mainstream

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

you've done some great articles on this topic and my experience aligns with your view completely.
Post reply on HN