Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Toward automated verification of unreviewed AI-generated code

peterlavigne.com

Post reply on HN
Print view View original

81–90 of 100 posts

Re: Toward automated verification of unreviewed AI-generated code

#81

Post by skydhash »

raw_anon_1111 wrote: post #71
jryio wrote: post #8

This is a naïve approach, not just because it uses FizzBuzz, but because it ignores the fundamental complexity of software as a system of abstractions. Testing often involves understanding these abstractions and testing for/against them. For those of us with decades of experience and who use coding agents for hours per-day, we learned that even with extended context engineering these models are not magically covering…

He’s saying you should write or at least have the LLM write the tests and you carefully review the tests and not the code.

That’s like saying to trace a spline, you only need to place a few points, carefully verify that the spline pass by those points and not verify the actual formula for the spline.

Or in other words: Test only guarantees their own result, not the code. The value of the test is because you know the code is trying to solve the general problem, not the test’s assertions.

Re: Toward automated verification of unreviewed AI-generated code

#82

Post by bluefirebrand »

softwaredoug wrote: post #64

When you write enough tests to verify AI code, you’re just making the tests the code and compiling an executable from tests https://softwaredoug.com/blog/2026/03/10/the-tests-are-the-c...

Which sucks because writing tests is the most tedious part of building software

Re: Toward automated verification of unreviewed AI-generated code

#83

Post by bizzletk »

fcatalan wrote: post #67

A couple weeks ago on a lark I asked Claude/Gemini/Codex to hallucinate a language they would like to program in and they always agreed on strong types, contracts, verification, proving and testing. So they ended up brainstorming a weird Forth-like with all those on top. I then kept prodding for an implementation and burned my weekly token budget until a lot of the language worked. They called it Cairn. So now I prom…

How would you compare it to similar things in this space like Mog?

https://news.ycombinator.com/item?id=47312728

Re: Toward automated verification of unreviewed AI-generated code

#84

Post by raw_anon_1111 »

skydhash wrote: post #81
raw_anon_1111 wrote: post #71

Earlier quoted context omitted.

He’s saying you should write or at least have the LLM write the tests and you carefully review the tests and not the code.

That’s like saying to trace a spline, you only need to place a few points, carefully verify that the spline pass by those points and not verify the actual formula for the spline. Or in other words: Test only guarantees their own result, not the code. The value of the test is because you know the code is trying to solve the general problem, not the test’s assertions.

That’s a horrible analogy. He specifically said he was designing and validating the tests based on his knowledge of what the goal of the project was.

Re: Toward automated verification of unreviewed AI-generated code

#85

Post by vemv »

What is a correct, bug-free program?

...It's one that does what a specific set of humans want. There's no other useful definition. One man's feature is another's bug.

It logically follows that there must be a human review step. How else would you know what the human wants, with sufficient detail?

Otherwise, there's an infinite number of undesired programs with passing test suites that AI can generate for you.

Re: Toward automated verification of unreviewed AI-generated code

#86

Post by Gigachad »

icoder wrote: post #73
Gigachad wrote: post #65

Earlier quoted context omitted.

I don't believe the junior devs on my team even run the code they are generating, let alone read it. Feeling like I'm doing 5x the work reviewing and testing that the person submitting has.

And I bet the impact of your review work on their development into medior/senior goes towards 0. I recognize this discrepancy where review effort becomes more than the coding itself. I don't think I could sustain that for long.

I have been looking at some way to reduce the burden on me and put it back on the developer submitting. So far I’ve been asking them to split their wall of code PRs down in to multiple smaller ones, and soon I’ll probably ask them to demo to me the feature working because I can’t assume they did this themselves.

Re: Toward automated verification of unreviewed AI-generated code

#87

Post by SAI_Peregrinus »

hrmtst93837 wrote: post #16
sharkjacobs wrote: post #7

I'm having a hard time wrapping my head around how this can scale beyond trivial programs like simplified FizzBuzz.

[flagged]

Or anything where the interaction of small pure functions matters. NAND is a simple pure function. 6 NANDs connected correctly gets you a D flip flop, and suddenly you've got state. Bugs can hide in the combinatorics of all the possible states of your system, and you'll never test them all in polynomial time.

Re: Toward automated verification of unreviewed AI-generated code

#88

Post by SAI_Peregrinus »

pron wrote: post #22

> The code must pass property-based tests Who writes the tests? It can be ok to trust code that passes tests if you can trust the tests. There are, however, other problems. I frequently see agents write code that's functionally correct but that they won't be able to evolve for long. That's also what happened with Anthropic's failed attempt to have agents write a C compiler (not a trivial task, but far from an excepti…

If you don't trust agents not to "cheat" the tests then:

The agent that writes the tests must have read-only access to the spec & the API. It MUST NOT have access to the implementation, even to read it.

The agent that writes the implementation must have read-only access to the spec. It MUST NOT have access to the tests implementation, only to the output report from running them.

This is a PITA to manage with classic UNIX permissions, but is doable with ACLs (`setfacl`/`getfacl`). Actually getting the agent processes to run as different users in an IDE setting instead of a CLI is not supported out of the box by any of the major vendors AFAICT, so IMO they're not really fit-for-purpose.

Re: Toward automated verification of unreviewed AI-generated code

#89

Post by fcatalan »

bizzletk wrote: post #83
fcatalan wrote: post #67

A couple weeks ago on a lark I asked Claude/Gemini/Codex to hallucinate a language they would like to program in and they always agreed on strong types, contracts, verification, proving and testing. So they ended up brainstorming a weird Forth-like with all those on top. I then kept prodding for an implementation and burned my weekly token budget until a lot of the language worked. They called it Cairn. So now I prom…

How would you compare it to similar things in this space like Mog? https://news.ycombinator.com/item?id=47312728

Same originating idea: "a language for AI to write in" but then everything else is different.

The features of both are quite orthogonal. Cairn is a general purpose language with features that help in writing probably working code. Mog is more like "let's constraint our features so bad code can't do much but trade that for good agent ergonomy".

Cairn is a crazy sprawling idea, Mog is a little attempt at something limited but practical.

Mog seems like something someone has thought about. No one has thought about Cairn, it's pure LLM hallucination, the fact that it exists and can do a lot of stuff it's just the result of someone (me) not knowing when a joke has gone too far.

Re: Toward automated verification of unreviewed AI-generated code

#90

Post by seanmcdirmid »

jryio wrote: post #8

This is a naïve approach, not just because it uses FizzBuzz, but because it ignores the fundamental complexity of software as a system of abstractions. Testing often involves understanding these abstractions and testing for/against them. For those of us with decades of experience and who use coding agents for hours per-day, we learned that even with extended context engineering these models are not magically covering…

If you wrote a spec for a memory allocator and asked the AI to identify edge cases and points that need to be tested first, it could work (I never asked AI to do that, but it works for other problems I’ve done). Yes, but you can’t feed in a garbage prompt and context and expect magically good tests to come out of that.
Post reply on HN