Live data from Hacker News

When AI writes the software, who verifies it?

leodemoura.github.io

111–120 of 309 posts

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

#111
post #42

I encourage everyone to RTFA and not just respond to the headline. This really is a glimpse into where the future is going. I've been saying "the last job to be automated will be QA" and it feels more true every day. It's one thing to be a product engineer in this era. It's another to be working at the level the author is, where code needs to be verifiable. However, once people stop vibing apps and start vibing kerne…

I am as enthusiastic about formal methods as the next guy, but I very much doubt any LLM-based technique will make it economical to write a substantial fraction of application software in Lean. The LLM can play a powerful heuristic role in searching for proof-bearing code in areas where there is good training data. Unfortunately those areas are few and far between. Moreover, humans will still need to read even rigoro…

This assumes everything about current capabilities stay static, and it wasn't long ago before LLMs couldn't do math. Many were predicting the genAI hype had peaked this time last year.

If you want it to be a question of economics, I think the answer is in whether this approach is more economical than the alternative, which is having people run this substrate. There's a lot of enthusiasm here and you can't deny there has been progress.

I wouldn't be so quick to doubt. It costs nothing to be optimistic.

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

#112
post #60

Earlier quoted context omitted.

https://en.wikipedia.org/wiki/Clarke's_three_laws

No i get the clarke reference. But how is an agent a dsl?

Maybe not an agent exactly but I can see an agentic application is kind of like a dsl because the user space has a set of queries and commands they want to direct the computer to take action but they will describe those queries and commands in English and not with normal programming function calls

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

#113

Earlier quoted context omitted.

If the code is well architected, the contract between C and D should make it clear whether changes in D affect C or not. And if C is not affected, then B and A won't be either.

> If the code is well architected Big constraint. Code changes, initial architecture could have been amazing, but constantly changing business requirements make things messy. Please don't use, "In ideal world" examples :) Because they are singular in vast space of non-ideal solutions

In that case your problem is bigger than just reviewing changes. You need to point the fingers at the bad code and bad architecture first.

There's no way to make spaghetti code easy to review.

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

#114
Formal verification gets you to deploy with confidence but it's still a snapshot. What happens when real-world inputs drift from what you tested against? The subtler problem is runtime behavioral drift: an agent that's technically correct but consistently misunderstands a whole class of user queries is invisible to any pre-deploy check. Pre-deploy and post-deploy verification are genuinely different problems.

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

#115
post #51

Earlier quoted context omitted.

I don't quite follow - are you describing an issue with the way your team has structured PRs? IMO, a PR should contain just enough code to clearly and completely solve "a thing" without solving too much at once. But what this means in practice depends on the team, product, velocity, etc. It sounds like your PRs might be broken up into too small of chunks if you can't understand why the code is being added.

I am saying PRs I get are around 60-70 lines of change, which is small enough to be considered as single unit (add to this unit tests which must pass with new change, so we are talking about 30 line change + 30 line unit test) But when looking at the PR changes, you don't always see whole picture because review subjects (code lines) are scattered across files and methods, and GitHub also shows methods and files parti…

check out the branch. if the changes are that risky, the web ui for your repository host is not suitable for reviewing them.

the rest of your issues sound architectural.

if changes are breaking contracts in calling code, that heavily implies that type declarations are not in use, or enumerable values which drive conditional behavior are mistyped as a primitive supertype.

if unit tests are not catching things, that implies the unit tests are asserting trivial things, being written after the implementation to just make cases that pass based on it, or are mocking modules they don't need to. outside of pathological cases the only thing you should be mocking is i/o, and even then that is the textbook use for dependency injection.

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

#116

I just finished writing a post about exactly this. Software development, as the act of manually producing code, is dying. A new discipline is being born. It is much closer to proper engineering. Like an engineer overseeing the construction of a bridge, the job is not to lay bricks. It is to ensure the structure does not collapse. The marginal cost of code is collapsing. That single fact changes everything. https://no…

In what world do these new tools help with "laying bricks", but not with ensuring that the structure does not collapse? How is that work any more difficult than producing the software in the first place? It wasn't that long ago that these tools could barely produce a simple program. If you're buying into the promises of this tech, then what's stopping it from also being able to handle those managerial tasks much better than a human?

The seemingly profound points of your marketing slop article ignore that these new tools are not a higher level of abstraction, but a replacement of all cognitive work. The tech is coming for your job just as it is coming for the job of the "bricklayer" you think is now worthless. The work you're enjoying now is just a temporary transition period, not an indication of the future of this industry.

If you enjoy managing a system that hallucinates solutions and disregards every other instruction, that's great. When you reach a dead end with that approach, and the software is exposing customer data, or failing in unpredictable ways, hopefully you know some good "bricklayers" that can help you with that.

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

#117
post #11

I think the issue goes even deeper than verification. Verification is technically possible. You could, in theory, build a C compiler or a browser and use existing tests to confirm it works. The harder problem is discovery: how do you build something entirely new, something that has no existing test suite to validate against? Verification works because someone has already defined what "correct" looks like. There is po…

Well that's a problem the software industry has been building for itself for decades. Software has, since at least the adoption of "agile" created an industry culture of not just refusing to build to specs but insisting that specs are impossible to get from a customer.

I don’t want to put words in your mouth but I think I agree. It’s called requirements engineering. It’s hard, but it’s possible and waterfall works fine for many domains. Agile teams I see burning resources doing the same thing 2-3x or sprinting their way into major, costly architectural mistakes that would have been easily avoided by upfront planning and specs.

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

#120

Formal verification gets you to deploy with confidence but it's still a snapshot. What happens when real-world inputs drift from what you tested against? The subtler problem is runtime behavioral drift: an agent that's technically correct but consistently misunderstands a whole class of user queries is invisible to any pre-deploy check. Pre-deploy and post-deploy verification are genuinely different problems.

> What happens when real-world inputs drift from what you tested against?

The whole point of formal verification is that you don't test. You prove the program correct mathematically for any input.

> an agent that's technically correct but consistently misunderstands a whole class of user queries is invisible to any pre-deploy check

The agent isn't verifying the program. The agent is writing the code that proves the program correct. If the agent misunderstands, it fails to verify the program.

Post reply on HN