[HN Gopher] When AI writes the software, who verifies it?
       ___________________________________________________________________
        
       When AI writes the software, who verifies it?
        
       Author : todsacerdoti
       Score  : 86 points
       Date   : 2026-03-03 16:34 UTC (6 hours ago)
        
 (HTM) web link (leodemoura.github.io)
 (TXT) w3m dump (leodemoura.github.io)
        
       | rademaker wrote:
       | In his latest essay, Leonardo de Moura makes a compelling case
       | that if AI is going to write a significant portion of the world's
       | software, then verification must scale alongside generation.
       | Testing and code review were never sufficient guarantees, even
       | for human-written systems; with AI accelerating output, they
       | become fundamentally inadequate. Leo argues that the only
       | sustainable path forward is machine-checked formal verification
       | -- shifting effort from debugging to precise specification, and
       | from informal reasoning to mathematical proof checked by a small,
       | auditable kernel. This is precisely the vision behind Lean: a
       | platform where programs and proofs coexist, enabling AI not just
       | to generate code, but to generate code with correctness
       | guarantees. Rather than slowing development, Lean-style
       | verification enables trustworthy automation at scale.
        
       | righthand wrote:
       | No one really. Code is for humans to read and for machines to
       | compile and execute. Llms are enabling people to just write the
       | code and not have anyone read it. It's solving a problem that
       | didn't really exist (we already had code generators before llms).
       | 
       | It's such an intoxicating copyright-abuse slot machine that a
       | buddy who is building an ocaml+htmx tree editor told me "I always
       | get stuck and end up going to the llm to generate code. Usually
       | when I get to the html part." I asked if he used a debugger
       | before that, he said "that's a good idea".
        
         | galbar wrote:
         | This is something I've been wondering about...
         | 
         | If boilerplate was such a big issue, we should have worked on
         | improving code generation. In fact, many tools and frameworks
         | exist that did this already:
         | 
         | - rails has fantastic code generation for CRUD use cases
         | 
         | - intelliJ IDEs have been able to do many types of refactors
         | and class generation that included some of the boilerplate
         | 
         | I haven't reached a conclusion on this train of thought yet,
         | though.
        
           | righthand wrote:
           | Pre-llm corpos my thoughts were that we should be training
           | juniors on code generators. Instead we're somewhere between
           | rtfm or dont.
        
       | acedTrex wrote:
       | No one does currently, and its going to take a few very painful
       | and high profile failures of vital systems for this industry to
       | RELEARN its lesson about the price of speed.
       | 
       | In fact it will probably need to happen a few times PER org for
       | the dust to settle. It will take several years.
        
         | arscan wrote:
         | Sure but industry cares about value (= benefit - price), not
         | just price. Price could be astronomical, but that doesn't
         | matter if benefit is larger.
        
         | jcgrillo wrote:
         | I feel like people used to talk about nines of uptime more. As
         | in more than one. These days we've lost that:
         | https://bsky.app/profile/jkachmar.com/post/3mg4u3e6nak2p
         | 
         | I recall a time, maybe around 2013-2017, when people were
         | talking about 4 or 5 nines. But sometime around then the
         | goalposts shifted, and instead of trying to make things as
         | reliable as possible, it started becoming more about seeing how
         | unreliable they can get before anyone notices or cares. It
         | turns out people will suffer through a lot if there's some
         | marginal benefit--remember what personal computers were like in
         | the 1990s before memory protection? Vibe coding is just another
         | chapter in that user hostile epic. Convenient reliability, like
         | this author describes, (if it can be achieved) might actually
         | make things better? But my money isn't on that.
        
       | foolfoolz wrote:
       | no one wants to believe this but there will be a point soon when
       | an ai code review meets your compliance requirements to go to
       | production. is that 2026? no. but it will come
        
         | righthand wrote:
         | We already have specifications though, so that's not different.
         | What happens when the AI is wrong and wont let anyone deploy to
         | production?
        
       | oakpond wrote:
       | You do. Even the latest models still frequently write really
       | weird code. The problem is some developers now just submit code
       | for review that they didn't bother to read. You can tell. Code
       | review is more important than ever imho.
        
         | MrDarcy wrote:
         | It is remarkably effective to have Claude Code do the code
         | review and assign a quality score, call it a grade, to the
         | contribution derived from your own expectations of quality.
         | 
         | Then don't even bother looking at C work or below.
        
           | NitpickLawyer wrote:
           | IME it works even better if you use another model for review.
           | We've seen code by cc and review by gpt5.2/3 work very well.
           | 
           | Also works with planning before any coding sessions. Gemini +
           | Opus + GPT-xhigh works to get a lot of questions answered
           | before coding starts.
        
         | sausagefeet wrote:
         | I agree with you. But I have to say, it is an uphill battle and
         | all the incentives are against you.
         | 
         | 1. AI is meant to make us go faster, reviews are slow, the AI
         | is smart, let it go.
         | 
         | 2. There are plenty of AI maximizers who only think we should
         | be writing design docs and letting the AI go to town on it.
         | 
         | Maybe, this might be a great time to start a company. Maximize
         | the benefits of AI while you can without someone who has never
         | written a line of code telling you that your job is going to
         | disappear in 12 months.
         | 
         | All the incentives are against someone who wants to use AI in a
         | reasonable way, right now.
        
           | redhed wrote:
           | I actually agree with good time to start a company. Lot of
           | available software engineers that can actually understand
           | code, AI at a level that can actually speed up development,
           | and so many startups focusing on AI wrapper slop that you can
           | actually make a useful product and separate yourself from the
           | herd.
           | 
           | Or you can be a grifter and make some AI wrapper yourself and
           | cash out with some VC investment. So good time for a new
           | company either way.
        
             | johnmaguire wrote:
             | It's gonna be like that HBO Silicon Valley bit again, where
             | everyone and their doctor is telling you about their app.
        
         | xienze wrote:
         | > The problem is some developers now just submit code for
         | review that they didn't bother to read.
         | 
         | Can you blame them? All the AI companies are saying "this does
         | a better job than you ever could", every discussion topic on AI
         | includes at least one (totally organic, I'm sure) comment along
         | the lines of "I've been developing software for over twenty
         | years and these tools are going to replace me in six months.
         | I'm learning how to be a plumber before I'm permanently
         | unemployed." So when Claude spits out something that seems to
         | work with a short smoke test, how can you blame developers for
         | thinking "damn the hype is real. LGTM"?
        
           | jf22 wrote:
           | I'm an 99% organic person (I suppose I have tooth fillings)
           | and the new models write code better than I do.
           | 
           | I've been using LLMS for 14+ months now and they've exceeded
           | my expectations.
        
             | xienze wrote:
             | So are you learning a trade? Or do you somehow think you'll
             | be one of the developers "good enough" to remain employed?
        
               | jf22 wrote:
               | I have a physical goods side hustle already and I'm
               | brainstorming ideas about a trade I can do that will
               | benefit from my programming experience.
               | 
               | I'm thinking HVAC or painting lines in parking lots. HVAC
               | because I can program smart systems and parking lot lines
               | because I can use google maps and algos to propose more
               | efficient parking lot designs to existing business
               | owners.
               | 
               | There is that paradox when if something becomes cheaper
               | there is more demand so we'll see what happens.
               | 
               | Finally, I'm a mediocre dev that can only handle 2-3
               | agents at a time so I probably won't be good enough.
        
             | HoldOnAMinute wrote:
             | Not only do they exceed expectations, but any time they
             | fall down, you can improve your instructions to them. It's
             | easy to get into a virtuous cycle.
        
           | bluefirebrand wrote:
           | > Can you blame them?
           | 
           | Yes I absolutely can and do blame them
        
         | bradleykingz wrote:
         | But it's so BORING. AI gets to do the fun part (writing code)
         | and I'm stuck with the lame bits.
         | 
         | It's like watching someone else solve a puzzle, or watching
         | someone else play a game vs playing it yourself (at least
         | that's half as interesting as playing it through)
        
           | lukan wrote:
           | For me the most fun part is getting something that works.
           | Design the goal, but not micromanage and get lost in the
           | details. I love AI for that, but it is hard really owning
           | code this way. (At least I manually approve every or most
           | changes, but still, verifying is hard).
        
             | bitwize wrote:
             | AI has really sharpened the line between the Master
             | Builders of the world and the Lord Businesses along this
             | question: What, exactly, is the "fun part" of programming?
             | Is it simply having something that works? Or is it the
             | process of going from not having it to having it through
             | your own efforts and the sum total of decisions you made
             | along the way?
        
           | HoldOnAMinute wrote:
           | I am really enjoying making requirements docs in an iterative
           | process. I have a continuous improvement loop where I use the
           | implementation to test out the docs. If I find a problem with
           | the docs, I throw away the implementation, improve the docs,
           | then re-implement. The kind of docs I'm getting are of
           | _amazing_ quality.
        
           | nz wrote:
           | Your workplace has chosen to deprive you of the enjoyment
           | that you got from the work. You have a few options: (1) ask
           | for a raise proportional to the percentage of enjoyment that
           | you lost, (2) find a workplace that does not do this, or (3)
           | phone it in (they see you and your craft as something be
           | milked for cash, so maybe stop letting yourself get milked,
           | and milk them right back, by doing _exactly_ what is asked of
           | you and _not_ more -- let these strategic geniuses strategize
           | using their own brains).
        
           | stretchwithme wrote:
           | I can solve a problem in 10% of the time. Dealing with an
           | issue TODAY, instead of having to put it in the backlog.
        
           | mosura wrote:
           | LLMs are still not good at structurally hard problems, and it
           | is doubtful they ever will be absent some drastic extension.
           | (Including continuous learning). In the mean time the trick
           | is creating a framework where you can walk them through the
           | exact stages you would to do it, only it goes way faster. The
           | problem is many people stop at the first iteration that looks
           | like it works and then move on, but you have to keep pushing
           | in the same way you do with humans.
           | 
           | Bluntly though, if what you were doing was CRUD boilerplate
           | then yeah it is going to just be a review fest now, but that
           | kind of work always was just begging to be automated out one
           | way or another.
        
         | throwaw12 wrote:
         | > You do
         | 
         | I really want to say: "You are absolutely right"
         | 
         | But here is a problem I am facing personally (numbers are
         | hypothetical).
         | 
         | I get a review request 10-15/day by 4 teammates, who are
         | generating code by prompting, and I am doing same, so you can
         | guess we might have ~20 PRs/day to review. now each PR is
         | roughly updating 5-6 files and 10-15 lines in each.
         | 
         | So you can estimate that, I am looking at around 50-60 files,
         | but I can't keep the context of the whole file because change I
         | am looking is somewhere in the middle, 3 lines here, 5 lines
         | there and another 4 lines at the end.
         | 
         | How am I supposed to review all these?
        
           | johnmaguire wrote:
           | 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.
        
             | throwaw12 wrote:
             | 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 partially making it even more difficult
             | to quickly spot the context around those updated lines.
             | 
             | Its difficult problem, because even if GitHub shows whole
             | body of the updated method or a file, you still don't see
             | grand picture.
             | 
             | For example: A (calls) -> B -> C -> D
             | 
             | And you made changes in D, how do you know the side effect
             | on B, what if it broke A?
        
               | cesarb wrote:
               | > Its difficult problem, because even if GitHub shows
               | whole body of the updated method or a file, you still
               | don't see grand picture.
               | 
               | > For example: A (calls) -> B -> C -> D
               | 
               | > And you made changes in D, how do you know the side
               | effect on B, what if it broke A?
               | 
               | That's poor encapsulation. If the changes in D respect
               | its contract, and C respects D's contract, your changes
               | in D shouldn't affect C, much less B or A.
        
               | FartyMcFarter wrote:
               | 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.
        
           | jra_samba wrote:
           | Tests. All changes must have tests. If they're generating the
           | code, they can generate the tests too.
        
             | throwaw12 wrote:
             | who reviews the tests? again me? -> that's exactly why I am
             | saying review is a bottleneck, especially with current
             | tooling, which doesn't show second order impacts of the
             | changes and its not easy to reason about when method gets
             | called by 10 other methods with 4 level of parent hierarchy
        
           | ptnpzwqd wrote:
           | If reviewing has become the bottleneck, the obvious - albeit
           | slightly boring - solution is to slow down spitting out new
           | code, and spend relatively more time reviewing.
           | 
           | Just going ahead and piling up PRs or skipping the review
           | process is of course not recommended.
        
             | throwaw12 wrote:
             | you are not wrong, but solution you are proposing is just
             | throttling the system because of the bottleneck, and it
             | doesn't solve the bottleneck problem.
        
         | [deleted]
        
       | _pdp_ wrote:
       | 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 possible a spec, or a reference
       | implementation, or a set of expected behaviours. The system just
       | has to match them.
       | 
       | But truly novel creation does not have ground truth to compare
       | against and no predefined finish line. You are not just solving a
       | problem. You are figuring out what the problem even is.
        
         | Avshalom wrote:
         | 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.
        
           | daveguy wrote:
           | Agile hasn't been insisting that specs are impossible to get
           | from a customer. They have been insisting that getting specs
           | from a customer is best performed as a dynamic process. In my
           | opinion, that's one of agile's most significant
           | contributions. It lines up with a learning process that
           | doesn't assume the programmer or the customer knows the best
           | course ahead of time.
        
             | skydhash wrote:
             | And good luck when getting misaligned specs (communication
             | issues customer side, docs that are not aligned with the
             | product,...). Drafting specs and investigating failure will
             | require both a diplomat hat and a detective hat. Maybe with
             | the developer hat, we will get DDD being meaningful again.
        
           | pydry wrote:
           | Agile is a pretty badly defined beast at the best of times
           | but even the most twisted interpretation doesnt mean that.
           | It's mainly just a rejection of BDUF.
        
       | holtkam2 wrote:
       | At the end of the day you need humans who understand the business
       | critical (or safety critical) systems that underpin the
       | enterprise.
       | 
       | Someone needs to be held accountable when things go wrong.
       | Someone needs to be able to explain to the CEO why this or that
       | is impossible.
       | 
       | If you want to have AI generate all the code for your business
       | critical software, fine, but you better make sure you understand
       | it well. Sometimes the fastest path to deep understanding is just
       | coding things out yourself - so be it.
       | 
       | This is why the truly critical software doesn't get developed
       | much faster when AI tools are introduced. The bottleneck isn't
       | how fast the code can be created, it's how fast humans can
       | construct their understanding before they put their careers on
       | the line by deploying it.
       | 
       | Ofc... this doesn't apply to prototypes, hackathons, POCs, etc.
       | for those "low stakes" projects, vibe code away, if you wish.
        
       | lgl wrote:
       | I'm in the process of building v2.0 of my app using opus 4.6 and
       | largely agree with this.
       | 
       | It's pretty awesome but still does a lot of basic idiotic stuff.
       | I was implementing a feature that required a global keyboard
       | shortcut and asked opus to define it, taking into account not to
       | clash with common shortcuts. He built a field where only one
       | modifier key was required. After mentioning that this was not
       | safe since users could just define CTRL+C for the shortcut and we
       | need more safeguards and require at least two modifier keys I got
       | the usual "you're absolutely right" and proceeded to require two
       | modifier keys. But then it also created a huge list of common
       | shortcuts into a blacklist like copy, cut, paste, print, select
       | all, etc.. basically a bunch of single modifier key shortcuts.
       | Once I mentioned that since we're already forcing two modifier
       | keys that's useless it said I'm right again and fixed it.
       | 
       | The counter point of this idiocy is that it's very good overall
       | at a lot of what is (in my mind) much more complicated stuff.
       | It's a .NET app and stuff like creating models, viewmodels,
       | usercontrols, setting up the entire hosting DI with pretty much
       | all best practices for .net it does it pretty awesomely.
       | 
       | tl;dr is that training wheels are still mandatory imho
        
       | indymike wrote:
       | Because of the scale of generated code, often it is the AI
       | verifying the AI's work.
        
         | tartoran wrote:
         | So who's verifying the AI doing the verifying or is it yet
         | another AI layer doing that? If something goes wrong who's
         | liable, the AI?
        
           | visarga wrote:
           | You have 2 paths - code tests and AI review which is just
           | vibe test of LGTM kind, should be using both in tandem, code
           | testing is cheap to run and you can build more complex
           | systems if you apply it well. But ultimately it is the user
           | or usage that needs to direct testing, or pay the price for
           | formal verification. Most of the time it is usage, time
           | passing reveals failure modes, hindsight is 20/20.
        
         | ptnpzwqd wrote:
         | I of course cannot say what the future holds, but current
         | frontier models are - in my experience - nowhere near good
         | enough for such autonomy.
         | 
         | Even with other agents reviewing the code, good test coverage,
         | etc., both smaller - and every now and then larger - mistakes
         | make their way through, and the existence of such mistakes in
         | the codebase tend to accellerate even more of them.
         | 
         | It for sure depends on many factors, but I have seen enough to
         | feel confident that we are not there yet.
        
       | simonw wrote:
       | The "Nearly half of AI-generated code fails basic security tests"
       | link provided in this piece is not credible in my opinion. It's a
       | _very_ thinly backed vendor report from a company selling
       | security scanning software.
        
       | muraiki wrote:
       | The article says that AWS's Cedar authorization policy engine is
       | written in Lean, but it's actually written in Dafny. Writing
       | Dafny is a lot closer to writing "normal" code rather than the
       | proofs you see in Lean. As a non-mathematician I gave up pretty
       | early in the Lean tutorial, while in a recent prototype I learned
       | enough Dafny to be semi-confident in reviewing Claude's Dafny
       | code in about half a day.
       | 
       | The Dafny code formed a security kernel at the core of a service,
       | enforcing invariants like that an audit log must always be
       | written to prior to a mutating operation being performed. Of
       | course I still had bugs, usually from specification problems
       | (poor spec / design) or Claude not taking the proof far enough
       | (proving only for one of a number of related types, which could
       | also have been a specification problem on my part).
       | 
       | In the end I realized I'm writing a bunch of I/O bound glue code
       | and plain 'ol test driven development was fine enough for my
       | threat model. I can review Python code more quickly and
       | accurately than Dafny (or the Go code it eventually had to link
       | to), so I'm back to optimizing for humans again...
        
       | yoaviram wrote:
       | 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://nonstructured.com/zen-of-ai-coding/
        
         | MattDaEskimo wrote:
         | Accountability then
        
           | yoaviram wrote:
           | Anticipating modes of failure, creating tooling to identify
           | and hedge against risks.
        
         | skydhash wrote:
         | > I just finished writing a post about exactly this. Software
         | development, as the act of manually producing code, is dying.
         | 
         | It was never that. Take any textbook on software engineering
         | and the focus was never the code, but on systems design and
         | correctness. I'm looking at the table of contents of one
         | (Software Engineering by David C. Kung) and these are a few
         | sample chapters:                 ...       4. Software
         | Requirement Elicitation       5. Domain Modelling       6.
         | Architectural Design       ...         8. Actor-System
         | Interaction Modeling       9. Object Interaction Modeling
         | ...       15. Modeling and Design of Rule-Based Systems
         | ...       19. Software Quality Assurance       ...       24.
         | Software Security
         | 
         | What you're talking about was coding, which has never been the
         | bottleneck other than for beginners in some programming
         | languages.
        
         | shinycode wrote:
         | Our CEO, an expert in marketing has discovered Claude Code and
         | is the one having the most open PR of all developers and is
         | pushing for us to << quickly review >>. He does not understand
         | why review are so slow because it's << the easiest part >>. We
         | live in a new world.
        
       | bitwize wrote:
       | Also AI.
        
       | madrox wrote:
       | 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 kernels, it really does
       | fundamentally change the game.
       | 
       | I also have another saying: "any sufficiently advanced agent is
       | indistinguishable from a DSL." I hadn't considered Lean in this
       | equation, but I put these two ideas together and I feel like
       | we're approaching some world where Lean eats the entire agentic
       | framework stack and the entire operating system disappears.
       | 
       | If you're thinking about building something today that will still
       | be relevant in 10 years, this is insightful.
        
         | charlieflowers wrote:
         | > "any sufficiently advanced agent is indistinguishable from a
         | DSL."
         | 
         | I don't quite follow but I'd love to hear more about that.
        
           | esafak wrote:
           | https://en.wikipedia.org/wiki/Clarke's_three_laws
        
           | jpollock wrote:
           | If the llm is able to code it, there is enough training data
           | that youight be better off in a different language that
           | removes the boilerplate.
        
         | bwestergard wrote:
         | 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 rigorously proved
         | code if only to suss out performance issues. And training
         | people to read Lean will continue to be costly.
         | 
         | Though, as the OP says, this is a very exciting time for
         | developing provably correct systems programming.
        
         | fmbb wrote:
         | There are still no successful useful vibe codes apps. Kernels
         | are pretty far away I think.
        
           | GoatInGrey wrote:
           | To be fair, Claude Code is vibe-coded. It's a terrible piece
           | of software from an engineering (and often usability)
           | standpoint, and the problems run deeper than just the choice
           | of JavaScript. But it is good enough for people to get what
           | they want out of it.
        
       | 50lo wrote:
       | One thing that seems under-discussed in this space is the shift
       | from verifying programs to verifying generation processes.
       | 
       | If a piece of code is produced by an agent loop (prompt -> tool
       | calls -> edits -> tests), the real artifact isn't just the final
       | code but the trace/pipeline that produced it.
       | 
       | In that sense verification might look closer to: checking
       | constraints on the generator (tests/specs/contracts), verifying
       | the toolchain used by the agent, and replaying generation under
       | controlled inputs.
       | 
       | That feels closer to build reproducibility or supply-chain
       | verification than traditional program proofs.
        
       | mentalgear wrote:
       | > Where this leads is clear. Layer by layer, the critical
       | software stack will be reconstructed with mathematical proofs
       | built in. The question is not whether this happens, but when.
        
       | boznz wrote:
       | This is the biggest problem going forward. I wrote about the
       | problem many times on my blog, in talks, and as premises in my
       | sci-fi novels
       | 
       | Sitting in your cubical with your perfect set of test suites,
       | code verification rules, SOP's and code reviews you wont want to
       | hear this, but other companies will be gunning for your market;
       | writing almost identical software to yours in the future from a
       | series of prompts that generate the code they want fast, cheap,
       | functionally identical, and quite possibly untested.
       | 
       | As AI gets more proficient and are given more autonomy
       | (OpenClaw++) they will also generate directly executable binaries
       | completely replacing the compiler, making it unreadable to a
       | normal human, and may even do this without prompts.
       | 
       | The scenario is terrifying to professional software developers,
       | but other people will do this regardless of what you think, and
       | run it in production, and I expect we are months or just a few
       | years away from this.
       | 
       | Source code of the future will be the complete series of prompts
       | used to generate the software, another AI to verify it, and an
       | extensive test suites.
        
         | skydhash wrote:
         | How do you get an extensive test suite?
        
         | Aldipower wrote:
         | If you need to interact with some things in
         | platform.openai.com, you know it is not months away, it is
         | there already now. I had to go through forms and flows there,
         | so buggy and untested, simply broken. They really eat their own
         | dog food. Interacting with the support, resulted in literally
         | weeks of ping pong between me and AI smoothed replies via email
         | to fix their bugs. Terrible.
        
       | bryanlarsen wrote:
       | You can use AI to make a reviewers job much easier. Add
       | documents, divide your MR into reviewable chunks, et cetera.
       | 
       | If reviewing is the expensive part now, optimize for
       | reviewability.
        
       | sslayer wrote:
       | State Sponsored Hackers AI will verify it.
        
       | chromaton wrote:
       | TFA seems to be big on mathematical proof of correctness, but how
       | do you ever know you're proving the right thing?
        
       | anonhacker199 wrote:
       | The biggest issue right now is most AI tools aren't hooked up
       | appropriately to an environment they can test in (Chrome
       | typically). Replit works extremely well because it has an
       | integrated browser and testing strategy. AI works very well when
       | it has the ability to check its own work.
        
       | slopinthebag wrote:
       | LLM generated code combined with formal verification just feels
       | like we're entering the most ridiculous timeline. We know formal
       | verification doesn't work at scale, hence we don't use it. We
       | might get fully vibe coded systems but we sure as hell won't be
       | able to verify them.
       | 
       | The collapse of civilisation is real.
        
       | bdcravens wrote:
       | The same ones who verify it when I write it: my customers in
       | production! /s (well, maybe /s)
        
       | ozten wrote:
       | This is really great and important progress, but Lean is still an
       | island floating in space. Too hard to get actual work done
       | building any real world system.
        
       | nemo44x wrote:
       | I believe the old ways, which agile destroyed, will come back
       | because the implementation isn't the hardest part now. Agile
       | recognized correctly that implementation was the hard part to
       | predict and that specification through requirements docs, UML,
       | waterfall, etc. were out of date by the time the code was cooked.
       | 
       | I don't think we'll get those exact things back but we will see
       | more specification and design than we do today.
        
         | bwestergard wrote:
         | Agile was a response to the coordination problems in certain
         | types of firms. Waterfall persisted in organizations that have
         | and require a more traditional bureaucratic structure.
         | Waterfall makes sense if you are building a space probe or an
         | unemployment insurance system, agile makes sense if you are
         | trying to find product market fit for a smartphone app.
        
       | dataviz1000 wrote:
       | 100% of my innovation for the past month has been getting the
       | coding agent to iterate with an OODA loop (I make it validate
       | after act step) trying to figure out how to get it to not stop
       | iterating.
       | 
       | For example, I have discovered there is a big difference between
       | prompting 'there is a look ahead bias' and 'there is a [T+1] look
       | ahead bias' where the later will cause it to not stop until it
       | finds the [T+1] look ahead bias. It will start to write scripts
       | that will `.shift(1)` all values and do statistical analysis on
       | the result set trying to find the look ahead bias.
       | 
       | Now, I know there isn't look ahead bias, but the point is I was
       | able to get it to iterate automatically trying different
       | approaches to solve the problem.
       | 
       | The software is going to verify itself eventually, sooner than
       | later.
        
       ___________________________________________________________________
       (page generated 2026-03-03 23:00 UTC)