>Except in "Brazil" it was a mechanical error in a deterministic machine caused by an invasive outside actor.

It was a literal bug in the computer. Metaphor as humor!

Ever deposit a check via PC browser?

With what? It's not exactly a fertile ground for growing things, and at the top of a hill.

> Will there be human oversight of the spec?

Well that's my suggestion, but I suppose nothing rules out an "all apprentices, no sorcerers" failure mode.

Verification debt has always been present, we just now feel an acute need for it, because we do it wrong.

Clause and friends represent an increase in coders, without any corresponding increase in code reviewers. It's a break in the traditional model of reviewing as much code as you submit, and it all falls on human engineers, typically the most senior.

Well, that model kinda sucked anyways. Humans are falliable and Ironies of Automation lays bare the failure modes. We all know the signs: 50 comments on a 5 line PR, a lonely "LGTM" on the 5000 line PR. This is not responsible software engineering or design; it is, as the author puts it, a big green "I'm accountable" button with no force behind it.

It's probably time for all of us on HN to pick up a book or course on TLA+ and elevate the state of software verification. Even if Claude ends up writing TLA+ specs too, at least that will be a smaller, simpler code base to review?