Comment by access97
21 hours ago
This is absolute bullshit.
These are bad-faith arguments toward "What about self modifying software".
Self modifying software has no grounds in reality or predictable behavior. It is an unreasonable expectation that software is magic. You would not fly on a self-modifying airplane. This is not a future i want to live in.
No; sorry, no.
The author, as a kid, believed computers where like a genie that could manifest anything they ask for. It seems to be a case of wishful thinking of a kid.
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...
Did he fall for it or does he see the dollar signs? Removing the bias of the article I do agree with some of his points. I actually wish we'd move away from Apple, Microsoft and Google and have more control. But as the author damn well knows: the masses will dig themselves a tar pit using AI in this way.
The author is smarter than falling for the hype, I think. But if not AI psychosis is a hell of a thing.
Why the hostility? The author has stated that he believes AI will alter how we think about operating systems. I don't think that's actually true, but I can see how this line of inquiry could lead to discoveries about how AI will change the line between installed software created by others and software that is "created" by users themselves. It's reasonable to suppose those discoveries in turn will result in new products. I wish him well and hope to hear more.
But I would use a self-modifying music player, editor, game, etc. It's not black and white as you are trying to paint.
As long as the software is proven correct, who cares how it achieves that?
How can it be proven correct if it's not deterministic? Isn't this the halting problem?
> How can it be proven correct if it's not deterministic?
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.
You seem a bit confused?
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.
Can't the non-deterministic LLM produce deterministic software? Assuming it is not allowed to modify the theorem proving software.
You're already living in it
Agreed. Read the article through and felt cringe most of the way through.