If you look at the proofs that Google solved, the fast one was similar to problems in Knuth, thus common in the corpus and the other two were reducible to exhaustive search, especially with lean4 feedback. Which is why they took more time than a human was given.
There results were impressive, but not sufficient for SWE.
If you note, it completely failed at the combinatorial problems.
SW engineering is details, nuance, and tradeoffs.
The specification problem that lead to an AI winter for expert systems still applies.
If we could create good, exhaustive contracts, programming is easy.
The failure of UML as a code generation tool is a good example.
As LLMs are good at pattern finding, at least within the simplicity bias problem, I do think that they will have utility.
But as an Enterprise Architect, form, complete specifications would completely remove the need for an LLM assistant as I could just write fitness functions and let the developers run with what they wanted.
As we know LLMs are in context learners built of threshold circuits, they simply don't have the ability to consider tradeoffs and details.
Funny enough this post has the smell of an author that wasn't aware of papers that came out in the previous couple years describing the specification problem.
I agree, I am also not interested in a system that replaces humans. I am interested in a system that automates the boring parts and makes SWE simpler and closer to classical engineering disciplines while keeping humans in the loop.
That is, an engineer would design and decompose the problem and the system would help to fill in the gaps in proofs. Sometimes this won't be possible, so the human engineer will need to redefine specifications or insert some intermediate lemmas.
There results were impressive, but not sufficient for SWE.
If you note, it completely failed at the combinatorial problems.
SW engineering is details, nuance, and tradeoffs.
The specification problem that lead to an AI winter for expert systems still applies.
If we could create good, exhaustive contracts, programming is easy.
The failure of UML as a code generation tool is a good example.
As LLMs are good at pattern finding, at least within the simplicity bias problem, I do think that they will have utility.
But as an Enterprise Architect, form, complete specifications would completely remove the need for an LLM assistant as I could just write fitness functions and let the developers run with what they wanted.
As we know LLMs are in context learners built of threshold circuits, they simply don't have the ability to consider tradeoffs and details.
Funny enough this post has the smell of an author that wasn't aware of papers that came out in the previous couple years describing the specification problem.