Well, hallucinations have been identified as an issue since the inception of LLMs, so this doesn’t appear true.
Indeed I expect to see a huge push into formally verified software just because sound mathematical proofs provide an excellent verifier to put into a LLM hardness. Just see how Aristotle has been successful at math, and it could be applied to coding too
Maybe Lean will become the new Python
"LLMs reliably fail at abstraction."
"This limitation will go away soon."
"Hallucinations haven't."
"I found a workaround for that."
"That doesn't work for most things."
"Then don't use LLMs for most things." "Autocomplete is great!"
"It doesn't work in bash"
"Then don't use it in bash."
I don't see what's wrong with this argument, and I certainly don't see it as a proof that the particular technology is actually useless, as you seem to be suggesting.