But it seems that he is falling for the LLM hype the same way. We all have the kid version of ourselves hiding somewhere within our grown versions, it seems...
The author is smarter than falling for the hype, I think. But if not AI psychosis is a hell of a thing.
Depends on domain, but basically all the same lessons we have for software written the old way by humans.
Which, ah, admittedly isn't great.
> Isn't this the halting problem?
No.
1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
First, the halting problem is only undecidable on arbitrary programs. Here we would be writing programs specifically to be easy to prove correct. In fact, we would be developing programs and proof at the same time.
Second, determinism is a nice property, but it's independent of whether you can proof software correct.
Have a look at eg randomised quicksort or the 'expected linear time minimum-spanning-tree algorithm' https://en.wikipedia.org/wiki/Expected_linear_time_MST_algor...
Or have a look at HyperLogLog. https://en.wikipedia.org/wiki/HyperLogLog
HyperLogLog only gives you a probabilistic approximation of the true number of distinct items. Here the proof would be about the probability that you are within some acceptable window around the true answer.