Three Posts, Forty-Eight Hours, One Argument
On July 28th and 29th, three separate items landed on the Hacker News front page. Read individually, each is a curiosity. Read together, they are the same argument arriving from three directions.
The first was a Show HN: a formally verified 3D mesh intersection algorithm written in Lean 4, at roughly 111 points and 48 comments. The interesting part wasn't the algorithm. It was the review instructions the author attached to it. Read the 93-line specification. Run the Lean checker. You never need to inspect the 1,000+ lines of implementation the AI wrote — or the 60,000+ lines of formal proof the agent generated along the way. The work was built mostly with Claude Opus 4.8, with some early proof strategies from Fable 5, and individual steps consumed 24+ hours of autonomous agent time.
The second was SpecForge, a platform for authoring formal specifications, at 61 points the same week.
The third was Robert C. Martin — Uncle Bob, the man who taught a generation of engineers to care about the shape of their code — posting that his current strategy is "to not read any of the code written by my agents." Fifty-three points, fifty-three comments, and eighteen months ago that sentence from that author would have been heresy.
It isn't anymore. But it also isn't the whole story, and the missing half is where founders get hurt.