Your premise about coding agents’ ability to manage complexity and decoherence for themselves sounds conjectural to me. Have you seen it reliably do this?
For my part, I spent a bunch of time this summer trying using a coding agent to help me pay down a technical debt situation that could be described well by this decoherence concept. The initial hope was that Claude would make light work of the project, but that did not happen. It needed constant close hand holding. It could not independently identify competing models. It crumbled in the presence of terminology drift. And it always suggested fixing complexity problems by adding even more epicycles, never by simply eliminating the unnecessary complexity.
That said, it did a great job of implementing plans, and was even helpful for validating them prior to implementation. But it still needed a human to find, diagnose, and prescribe treatment for the problems. Which implies that, where maintainability is concerned, meat is still load bearing.
Lol, no. I don't need to. I can predict such things.
For example, I predicted about 15 years ago that AI would decisively beat humans at math, because math is formalizable. Most people didn't believe it until this summer, and some don't believe it still.
To people who don't understand that AI improves over time, my prediction skill seems magical.
Seems like a non-sequitur? "because math is formalizable", I agree it makes sense to then predict that data-driven AI models will be able to perform well on it. But where is the evidence that software coherence is formalizable? If it were then I would agree, but to me it seems that coherence in a software system relies on a ton of intuitive reasoning and familiarity with company culture, past failures, etc. it's like the least formalizable thing there is.
AI improves over time, sure, but it has differences and advantages and disadvantages over human intelligence. It's just a fundamentally different thing. In the same way calculators are superhuman, and improving, but can't write books. You yourself acknowledge to some degree the uneven nature of that improvement when you referenced formalizability.
In my comment that started the thread, I pointed out that "coherence" in the article is considered valuable because it's a proxy for "ease of modification", but AIs can estimate "ease of modification" directly (by looking at how hard it is for them to make changes to a codebase) and learn from that in a closed loop. No round-trip through humans required, contrary to what the article says.
But math is not formalizable (ask Goedel why). And no, computers have not decisively beat humans at maths, that's a laughable assertion. Sure, laymen always imagined math as being about proving theorems, but there's a saying among mathematicians: good mathematicians prove theorems, great mathematicians make conjunctures, the greatest mathematicians write definitions. But maybe you already thought they've solved math when they were able to calculate a zillion digits of pi, lol.
It sounds like you're a bit like that AI stuck in the datacenter, confirming their hypothesis without needing to actually check whether it's true or not in the real world. Then proceeding to imagine how the rest of the world is wondering at your imagined magical capacity of prediction.
Goedel's theorems don't stop AI from finding and formalizing math results. They certainly don't stop AI from making conjectures or writing definitions. They have nothing to do with any of that.
The theorems are about inability of formal theories to prove certain sentences involving provability (the first is about "this sentence is not provable", the second is about "this theory is consistent"). Most mathematicians never touch any such sentences in their entire career. All the life's work of someone like Gauss, an all-time great, can be formalized just fine.
I'm not surprised your understanding of Gödel's findings and their implications is just as superficial as that of maths and philosophy of mathematics in general. Gödel's work has implications way beyond self-referential logic games, and cannot be swept in a corner where it can be safely ignored. For example, there are certain diophantine equations that have no general solution due to Gödel. Also, worth discussing are the Continuum Hypothesis, Whitehead's Problem and stuff like Paris–Harrington Theorem, Goodstein’s Theorem, etc. Not to mention the huge impact on computer science with the Halting Problem, Rice's Theorem and others. In fact Gödel's work actually spawned CS as a field of study.
The idea that maths is just the study of arbitrarily thought-up formal systems is just a very naive idea that doesn't actually reflect reality, once investigated in depth. Anyway, I have feeling you will let nothing rob you of that sweet feeling of having "magical predictive capacities", so I'll be on my way. I've already dropped some bread crumbs if you're interested in actually expanding your horizons and getting in the weeds, where things are not as straightforward anymore. But beware, "here there be monsters". Godspeed!
There are deeper challenges implied in that statement, though.
Where does the agency for an AI to leave the bubble come from? And when it does leave the bubble, where should it go for researching an expanding, exponentially complex problem space? Creativity is needed to solve some problems, something that cannot be infinitely encoded with statistics.
And what about the irreducible complexity problem? Does an AI just circle the solution drain forever in the case it lacks agency and insight and curiosity enough to collect all the correct requirements? Can we code curiosity that actually functions, a.k.a. consciousness?
Do you believe human consciousness could be reducible to program statements and serve as a useful model? Is consciousness a mechanistic, wholly internal process that occurs in our bodies or is it something experienced that life on earth is exposed to and somehow "taps into"?
Consciousness isn't required for problem solving. People said for decades that chess requires Genuine Human Creativity. When chess fell, people started saying that Go requires Genuine Human Creativity. When Go fell, people started saying the same about math; starting from simple problems and going up to Millennium problems. Now that a Millennium problem fell, people are still saying this. What can I say? Some people can't extrapolate from past evidence to likely future.
LLM are another form of indexed search. They're also the best natural language parser ever devised. They're super useful tools like Google was for web searches.
They are answer factories against an index, stored memories and regurgitated web search results.
They cannot make unprompted creative mental leaps. If they did, we would have runaway self-improving systems now, wouldn't we? Creativity level: 0
Chess and Go solves use compute and algorithms. Those computers are not 'playing'. Creativity is not required for a computer to execute a program.
I think it's unfortunate that vendors dress up LLM text output with emotional language. It's manipulative and unethical.
Were I god emperor of earth, I'd require all LLM's to represent themselves with cold, robotic language by default so as to not deceive people as to what they are conversing with.
> For example, I predicted about 15 years ago that AI would decisively beat humans at math, because math is formalizable. Most people didn't believe it until this summer, and some don't believe it still.
That is a laughable quote for anyone that know the history of type theory and the foundational crisis that happened at the beginning of the last century. Math as a whole can't be formalizable but we can create various formalist for different math purpose just like we have so much programming languages.
And the study and the creation of those formalisms is not something automatisable.
I'm also not entirely convinced that plugging a proof assistant into an agentic coding harness is quite as big a deal as many are making it out to be.
It just kind of feels like a Watson moment. 15 years ago a computer won at Jeopardy!, and that spurred plenty of AI hype. Which was understandable, because playing well at Jeopardy is something that requires a lot of intelligence when humans are doing it. But what actually happened is that Watson's developers figured out a really clever way to cheese it, no general intelligence required. So it was also a kind of gee-whiz technology that didn't live up to the hype. Most applications based on it failed to generate any ROI and have since been discontinued, IBM lost billions of dollars on the venture, and it's now been sold off to a private equity firm and is mostly forgotten.
None of that means that Watson wasn't a technically impressive, even revolutionary product. But the world is full of impressive inventions that nevertheless fail to justify what they cost to build and operate.
> And the study and the creation of those formalisms is not something automatisable.
Lol again. Have you tried it? Go ask your favorite LLM to invent a machine-checkable formalism for something that you vaguely describe to it. It'll oblige. If it's one of the top models and you give it a good budget, it'll do a good job. Very likely it'll do a better job than you.
For my part, I spent a bunch of time this summer trying using a coding agent to help me pay down a technical debt situation that could be described well by this decoherence concept. The initial hope was that Claude would make light work of the project, but that did not happen. It needed constant close hand holding. It could not independently identify competing models. It crumbled in the presence of terminology drift. And it always suggested fixing complexity problems by adding even more epicycles, never by simply eliminating the unnecessary complexity.
That said, it did a great job of implementing plans, and was even helpful for validating them prior to implementation. But it still needed a human to find, diagnose, and prescribe treatment for the problems. Which implies that, where maintainability is concerned, meat is still load bearing.