Diogenesian

That's not what I mean. I am talking about quirks and bugs that really are pretty subtle, and which really might turn up in e.g. a verified systems programming context: https://github.com/James-Hanson/junk-theorems-in-lean/blob/m... (there is a proof of 0=1 at the end - it is easy to understand where it comes from, but low-level compiler stuff like this is always a possibility.)

LLM agents will a) discover dumb counterintuitive stuff like this and b) exploit it to satisfy the kernel with c) the questionable lines being buried behind millions of lines of math slop. Humans have to check this stuff.

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct. But you gotta check.

This future of "the AI built the compiler and it's totally incomprehensible spaghetti, but don't worry, it verified the compiler works using this AI-generated proof assistant whose codebase is also pure spaghetti" terrifies me.

I think part of it is the perception that real environmental and public health damage is being done for totally trivial and indefensible causes. A data center is not like an airplane parts manufacturer, which has lots of ugly pollution but provides a necessary national service. Most people use generative AI recreationally, and the productivity gains among white-collar workers are awfully ephemeral. And if you're less pessimistic about the economics of generative AI... that makes it worse!

"We get a ton of money, you get increased natural gas emissions, increased unemployment, your electric bill is going up... oh and guess who's bailing us out when the bubble bursts?" Pretty rotten deal!

"Oops, I really should have checked GNU's policy on LLM code generation before submitting an LLM-generated patch. That was a stupid mistake: not only was my patch rejected, I publicly announced myself as a thoughtless blunderer who doesn't read the rules."

- from an alternate reality, where devs still have shame and humility