Live data from Hacker News

When AI writes the software, who verifies it?

leodemoura.github.io

241–250 of 309 posts

Re: When AI writes the software, who verifies it?

#241

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

> I have no constructive recommendations; I feel the industry will keep their foot on the pedal until something catastrophic happens

I can't wait. Maybe when shitty vibe coded software starts to cause real pain for people we can return to some sensible software engineering

I'm not holding my breath though

Re: When AI writes the software, who verifies it?

#242
At the end it mentions what the future engineers will do:

> Engineers spend more time writing specifications and models, designing systems at a higher level of abstraction, defining precisely what systems must do, what invariants they must maintain, what failures they must tolerate.

We do that already and the abstractions are very high. The other part is about knowing what the system is supposed to do way in advance, which is not how a lot of engineering is done because it is an exploratory problem. Very few of us write crypto or spend much time in a critical piece of code. And most importantly no user ever said if the software they buy is using proofs. Just like security these concerns are at the bottom of a barrel.

Re: When AI writes the software, who verifies it?

#243
What’s striking here is the convergence on a minimal axiomatic kernel (Lean) as the only scalable way to guarantee coherent reasoning. Some of us working on foundational physics are exploring the same methodological principle. In the “Functional Universe” framework[0], for example, we start from a small set of axioms and attempt to derive physical structure from that base.

The domains are different, but the strategy is similar: don’t rely on heuristics or empirical patching; define a small trusted core of axioms and generate coherent structure compositionally from there.

[0] https://voxleone.github.io/FunctionalUniverse

Re: When AI writes the software, who verifies it?

#244
post #110

It seems like sound testing methodology to identify important theorems related to the code, prove them, and then verify the proof. Verification gets sold as "bulletproof" but I'm skeptical for a couple reasons: - How do you establish the relationship between the code and the theorem? Lean theorem can be applied to zlib implemented in Lean, what if you want to check zlib implemented in a normal programming language li…

The article does not reveal it to me either how the existing code would be mapped to Lean and back. The impression from zlib example is that I'd be expected to program in Lean. No way it's going to happen. The language is too complex for me and my average colleague. We're also not going to have two parallel implementations in ordinary language and Lean and compare them with 'differential random testing' (see https://aws.amazon.com/blogs/opensource/lean-into-verified-s... someone linked in the discussion), that's just too taxing for bigger products, let alone we typically don't have enough time to do one implementation right.

The gap of having succinct, expressive, powerful and executable specification to be able to continuously verify AI-generated programs is real, but I don't see how Lean alone closes it. If the author's intention was to attract community to help build that out with Lean in the center, it's not clear to me where to even start. Since the author provided no hints or direction, I've a feeling it's not clear to them either.

Re: When AI writes the software, who verifies it?

#245

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

How about a subsequent review where a separate agent analyzes the original issue and resultant code and approves it if the code meets the intent of the issue. The principle being to keep an eye out for manual work that you can describe well enough to offload. Depending on your success rate with agents, you can have one that validates multiple criteria or separate agents for different review criteria.

Slop on slop. Who watches rhe watchman?

Re: When AI writes the software, who verifies it?

#246
post #164

Earlier quoted context omitted.

You are fighting nondeterministic behavior with more nondeterministic behavior, or in other words, fighting probability with probability. That doesn't necessarily make things any better.

Aren't human coders also nondeterministic? Assigning different agents to have different focuses has worked for me. Especially when you task a code reviewer agent with the goal of critically examining the code. The results will normally be much better than asking the coder agent who will assure you it's "fully tested and production ready"

Human coders are far more reliable. The only downside is speed, and therefore cost

Re: When AI writes the software, who verifies it?

#248

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

Long time ago in France the mainstream view by computer people was that code or compute weren't what's important when dealing with computers, it is information that matters and how you process it in a sensible way (hence the name of computer science in French: informatique. And also the name for computer: “ordinateur”, literally: what sets things into order).

As a result, computer students were talked a lot (too much for most people's taste, it seems) about data modeling and not too much about code itself, which was viewed as mundane and uninteresting until the US hacker culture finally took over in the late 2000th.

Turns out that the French were just right too early, like with the Minitel.

Re: When AI writes the software, who verifies it?

#249

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

Honestly, unit tests (at least on the front-end) are largely wasted time in the current state of software development. Taking the time that would have been spent on writing unit tests and instead using it to write functionally pure, immutable code would do much more to prevent bugs.

There's also the problem that when stack rank time comes around each year no one cares about your unit tests. So using AI to write unit tests gives me time to work on things that will actually help me avoid getting arbitrarily fired.

I wish that software engineers were given the time to write both clean code and unit tests, and I wish software engineers weren't arbitrarily judged by out of touch leadership. However, that's not the world we live in so I let AI write my unit tests in order to survive.

Re: When AI writes the software, who verifies it?

#250

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

At my job we have a requirement for 100% test coverage. So everyone just uses AI to generate 10,000 line files of unit tests and nobody can verify anything.

Exactly! It's frustrating how much developers get blamed for the outcomes of incompetent management.
Post reply on HN