Most of Wolfram's discussion of "bugs" is not about the following situation:
You want a program that does X. So you think about what a program that does X should look like, and write a program that does what you think should produce result X, but maybe you made some mistakes.
but about the following, to my mind completely different, situation:
You want a program that does X. So you write a bunch of random short programs and after a while you find one that looks on small examples as if it's doing X. You use that one, but maybe actually it doesn't always work.
The key difference here is that in the first case you try to make there not be bugs by understanding what the program is doing and in the second you try to make there not be bugs by looking at the program's output.
(Perhaps some super-extreme practitioners of test-driven development might argue for something like the latter. Perhaps some AI-driven programming is uncomfortably close to it. But it's not, generally, how people have produced and debugged software.)
Wolfram kinda tries to justify this perspective by saying:
"Fundamentally the only way to make sure a program will always do what you want is to understand everything it can do. But there’s a kind of paradox implicit in that: if you can really understand everything your program can do that basically means the program is doing something computationally reducible, and you probably in the end didn’t actually need to run the program with all its steps to get the result you wanted."
but I think this is silly (and suspect it's the result of Wolfram trying to shoehorn his pet notion of "computational (ir)reducibility" into places where it brings no actual insight). It happens all the time that you write a program that (at least in principle) you understand completely, but that you don't know a much cheaper way to do it.
mjburgess 1 days ago [-]
Computer scientists generally struggle with intensional contexts, ie., the sense in which sqrt(4) isnt (1 + 1); or the sense in which I believe(that sqrt(1101) ~10) but I dont believe(that 10^2 ~1101)
So they replace everything with extensional contexts, ie., in/out sets -- where things are replaceable by their values. And then use the machinery of very simple mathematics to analyse the situation.
In ML, consider comparing two classifiers extensionally, so that two classifiers "are the same" if they partition some input data exactly the same vs., declaring them different if they do so by means of some differing internal representation.
Since intensional contexts are the archetypal feature of mental representations, they're rarely analysed well by computer scientists.
zby 11 hours ago [-]
There are programs with proofs that they work - but that does not make them reducible.
I think its easy for us to think we can understand what a program is going to do when we're dealing with high level abstractions. I think if we really came to grips with everything the program is doing all the way down to the hardware level, we might have less confidence that we can predict what its going to do with 100% accuracy every time, even in the case of supposedly simple programs.
drdeca 4 hours ago [-]
Well, of course at the real hardware level there will be some non-zero amount of nondeterminism, but the error correction steps that have been implemented are enough to make the probability of it behaving contrary to the design of the hardware, low enough to be pretty negligible.
And if you want additional assurance (due to, e.g. the computation being very long) you could probably use some cryptographic techniques to produce a certificate that the output is as it should be, and you can check that certificate as many times as you want to avoid possible random hardware errors in the process of checking the certificate.
tomstuart 1 days ago [-]
At the risk of straying into forbidden metacommentary: look, I understand (and also feel) the temptation to have a go at Stephen Wolfram every time he posts something wacky, but… he’s just a guy with a fun hobby, isn’t he? Sure it’s all a bit eccentric and self-indulgent, but so are most hobbies, and in contrast to basically every other rich tech man he isn’t actually hurting anyone. Live and let live I reckon.
fasterik 1 days ago [-]
I'm sure there are unwarranted attacks on Stephen Wolfram out there in the public discourse, but what I see is people criticizing his ideas, which is always fair game.
I actually think criticism is especially important in the case of high-profile public figures like Wolfram. Far more people in the general public know about him and his highly speculative and unproven theories, while at the same time thousands of serious scientists publishing important and influential work go relatively unrecognized.
anitil 23 hours ago [-]
I appreciate this opinion, it's very generous
seanhunter 1 days ago [-]
One of the frustrating things with the way Stephen Wolfram works is because he never actually defines anything it’s very hard to pin down what is actually interesting empirical science and what is data visualisation buggering around.
Here, before he starts, how do we know that the bugs in the Turing machine implementation of f(n)=n+1 are in any way representative of bugs in a normal computation? He seems to be generating random state machines and then evaluating them and picking ones which are nearly but not quite correct implementations of f(n)=n+1. Is that like a normal “honest” software bug? Is it like a deliberate software sabotage like you might look for when evaluating a software supply chain risk? Is it like the sort of vulnerability you might see when fuzzing? As far as I can see, there’s no reason to think it’s like any of these.
More broadly, since the “Principle of Computational Equivalence” and “computational irreducibility” are referred to as touchstones but are never actually defined or properly established how are we supposed to treat them? Interesting conjectures? Actual axioms? Something in between?
PaulHoule 1 days ago [-]
I see it as related to the Church-Turing thesis which is also a bit fuzzy but I think comes down to the conjecture that there is no physical computer which exceeds the Turing machine in capabilities. (Quantum computers, as we know them, don't count because they can be simulated by classical computers with sufficient space and time)
One thing I find tragic about Wolfram is that he found his holy grail, Rule 30, at the very beginning of his project and ever since he's found that every family of rules that he's look at that is sufficiently powerful has something like Rule 30 -- but always a bit more complex, complicated and not quite so beautiful, in fact often outright ugly...
... so he jumps into this sort of thing and samples of some of a ruliad, finds the usual things he finds in every ruliad, gets excited about it and thinks he has a "theory" and then moves on to something else and most of us are scratching our heads.
seanhunter 1 days ago [-]
The Church-Turing hypothesis I agree could be crisper (ie the definition of effectively computable is a bit complicated/weasely), but it actually says something quite concrete that I can understand and potentially falsify ie that a universal turing machine, the lambda calculus and general recursion can all "effectively compute" the same things. That seems reasonable, and I can check that something I can write in lambda calculus I can compute on a Turing Machine (simulated at least).
Whereas in stating the Principle of Computational Equivalence Wolfram says things like "... the evolution of weather systems can, in principle, compute the same things as a computer."[1]
Well, ... wtf? What does it mean to say the evolution of a weather system can compute something? Where do we even start on understanding this? I pick up a calculator and compute the volume of a cone. It's a sunny day outside. How do I "in principle" use that to check my calculation? It literally makes no sense whatsoever on its face as a claim but it is so slippery because of that "in principle" that it doesn't give me anything to hold onto that I could even test.
And that's before I even get started on the "underpants gnome" logical justification behind the claim, which seems to be:
1. Computers are complex
2. Weather is complex
3. Therefore they are "in some sense" equivalent
4. <don't worry about step 4>
5. Thus weather can "in principle" compute the same things as a computer.
I'm really not trying to misrepresent him, I'm just baffled.
I'm of course hearing this second- or third-hand, but when I read 'evolution of weather systems' I substitute for 'cellular automata'/'Conway's game of life', vaguely recall them as being Turing-complete, then smile and nod and get back to ignoring the article.
PaulHoule 5 hours ago [-]
It's handwavy but I can't help but think that because of the way symbolic dynamics works that you can't find families of approximating functions inside turbulence even though I can't see it being practical, like sensitive dependence on initial conditions will make noise overwhelm your ability to take measurements. See
Isn't that also the point of your comment only much lazier?
marssaxman 24 hours ago [-]
Not sure how you get to "I think I am very smart" from "this guy thinks he is very smart, and his writing invariably highlights that belief to the detriment of whatever he's actually trying to communicate"...
For all I know, maybe he actually is the world-class genius he believes himself to be, but it's difficult to tell underneath all the blatant self-promotion.
The thing is, Wolfram is that smart, having gotten his Ph.D. at 20 or something. He's just never been humbled, had a leash put on him so he could be aimed and focused on productive work (outside of maybe Mathematica). Probably because a lot of university professors in the 80s were like "wow, that kid is smart" and indulged his ego. (One major exception: Richard Feynman! https://www.cantorsparadise.com/richard-feynmans-advice-to-a...)
After Quake was released and the principals of Id Software broke up, John Romero pretty much spent the next few years making an ass of himself during the development of Daikatana. When asked about the delayed and beleaguered development process on Slashdot, John Carmack kind of paid him a backhanded comment saying something like "A properly disciplined Romero is a credit to any team." And that's more or less what Wolfram is: properly disciplined, he would be an asset to any cutting-edge physics research team, but as he his he'd rather go down these rabbit holes than suffer to work with people of more ordinary intellect. And it's his, and the world's, loss really.
Athanase000 15 hours ago [-]
Every time something is posted from Wolfram I realize I am the only guy who likes him. Yes, he does not state, or prove, theorems. He is studying alien mathematics. Nobody has any idea of what is going on, neither does Wolfram, but he is trying! In the world of weird computability experiments he is the one with the least worst understanding of the matter. I think the fact that we have all these computational stuff laying around and we have no idea what's going on, and probably never will (by virtue of the halting theorem or something similar), contrasted with the incredible amount of understanding that normal mathematics has brought forth, is mind-boggling. You can create a turing machine from very simple rules, and nobody on earth will be able to tell what it's doing. And most machines will be like that! Most cellular automaton will be like that! Computational irreducibility is a fascinating philosophical idea. Even if it is kinda fruitless. To me it looks like there is this infinite world of meaningless computation, and then somewhere you have this happy path of actual mathematics which is full of meaning and absolutely makes sense. And somehow humans stumbled upon this happy path.
For me the ultimate proof that AI will have become super-intelligent is not that it will prove results that mathematicians can already deal with, it's that it will be able to look at a Turing machine and tell you "Yep, that's how it behaves, it follows these rules, and will never halt because this and that". I realize this is impossible in general, but if it's possible to some extent, where it is way better than the people over at busy beaver challenge, personally my mind will be blown.
dloss 1 days ago [-]
Am I wrong to conclude that the statement by Google's VP of Security Engineering that "we simply must eliminate every software vulnerability on Earth" (before AI Agents find them) is not only stunningly ambitious, but doomed from the start?
As in, there is no programming language complex enough to describe any program, that is not inherently complex enough to describe bugs? Sounds legit, how would one prove it? :)
drdeca 1 days ago [-]
Eh? I don’t see how Gödel’s results imply that.
wduquette 1 days ago [-]
At least not automatically. From an algorithmic standpoint it seems likely to be undecidable. But let us not look too closely at what was really a throwaway remark.
drdeca 4 hours ago [-]
It is true of course that there is no automatic procedure which takes in an arbitrary program and decides if it has a desired input/output behavior. (Whether an input program has a given “semantic property” is undecidable.)
But that doesn’t mean that it is impossible to have all our programs be formally verified. For that, if we have a formal specification for what each should do…
Well, I suppose it’s possible that some program we would want is possible to implement with the desired properties, but not possible to prove that it has those properties?
It is possible to enumerate (program, proof) pairs though.
WorldMaker 1 days ago [-]
It's my view of the Halting Problem that we've known for a surprisingly long time that eliminating all software bugs is mathematically impossible and should stop letting perfect get in the way of the good.
Especially with the more recent relative of the Halting Problem combined with the Church-Turing Theorem that found mathematical proof of a "0-day" sandbox escape in the Universal Turing Machine itself.
We have always lived in a house of glass. LLM agents automating trebuchets for rock throwing certainly seems like a bad idea to me and "let's simply eliminate all software vulnerabilities" an interesting bit of ostrich work (stick your head in the sand and hope it all gets better).
layer8 1 days ago [-]
This has little to do with the halting problem, because we can choose to not deploy programs (or subroutines) that we want to be terminating but can’t prove that they are terminating. And that goes for any undecidable problem. There is no application where we want the program to have a certain property where we would be forced to deploy a program where we can’t prove the property due to computational theory reasons.
No, the real issue is that for the most we don’t want to put the necessary effort into proving the relevant properties, because it’s costly and time-consuming, and we think we can live with the risk. The issue is not some theoretical inability to do so.
WorldMaker 1 days ago [-]
We absolutely have pragmatic compromises and shortcuts for dealing with termination problems, but that doesn't mean we've solved the Halting Problem, it means we've adapted to coexistence with it. (And maybe we've coexisted with the Problem for long enough it feels like most of those adaptations are sufficient day to day, which makes it all the harder to appreciate the bugs that are always there we just mitigate enough to worry about them less.)
Potentially Infinite Loops are a great power. We've learned in most programming languages the "Uncle Ben lesson" that with such great power, comes great responsibility. In most programming languages we don't want to remove the ability to infinitely loop, because we might need that power, we work on ways to limit that responsibility (loop guards and timeouts and cancellations and teardowns). But it will likely always be possible to see some code spin in a loop we can't tell is accidentally infinite or just a loop with a lot more work than we expected. The infinite spin wait will always be a risk in our code.
I think it has a lot to do with the Halting Problem.
layer8 1 days ago [-]
An infinite loop doesn’t mean that you can’t prove whatever property you want to prove about your program, if you’ve designed it for that. The limitations coming from undecidability don’t really affect our everyday applications. Unless your application is exactly to determine whether another arbitrary program will halt, that is. But that’s not what the vast majority of software whose bugs we might be concerned about is about.
“We can’t write bug-free software due to the halting problem anyway” is an incorrect argument.
WorldMaker 1 days ago [-]
You can't prove a program completed successfully if you can't prove a program even completes at all.
I don't know what properties you think people are trying to pragmatically prove about arbitrary programs but "did the program complete successfully" will always be an important, pragmatic property in software development. Especially in the pragmatic world where so much of our software is chaining smaller programs together to solve a task.
I'm saying we can't write perfectly bug-free software because of the Halting Problem and the inability to prove any given loop will not be infinite until running that loop. Perfect remains the enemy of the good and we certainly write a lot of "bug-free-enough" software without worrying about the Halting Problem day-to-day. But if you are saying the world needs to write perfectly bug free code starting tomorrow because LLMs will find all the vulnerabilities and sandbox escapes the Halting Problem is absolutely one of the reasons we can't ever provably hit that "perfect" target. We still need to find "good enough" or we give up on software development altogether and that's not what I'm advocating. Perfect is the enemy of the good. Mathematically perfect provably does not exist. Software will always have bugs, especially in the world with a threat model of active brute force machines.
voidmain 1 days ago [-]
I think you have slightly misunderstood the halting problem. There is no computer program H that, for every program P, determines whether P halts. This does not imply that for some particular program Q there is no proof that it halts. In fact in the setting where programs do not take input there is always such a proof (just a trace of the program running to completion). And there are many valid proofs of theorems like "For all x, Q(x) halts" for particular Q. Consider, for example, the case where Q has no control flow at all!
WorldMaker 24 hours ago [-]
I think it's more that I lean into some of the corollaries that directly factor computation time into account. There is no computer program H that for every program P determines whether P halts faster than running P.
You cannot find/prevent every case of an infinite loop at design time/compile time if the only way to determine a complex enough control flow converges towards halting is to run the full program in a live environment.
Veserv 1 days ago [-]
You have a serious misunderstanding of the consequences of the undecidability of the Halting Problem. The Halting Problem says you can not prove the precise halting behavior in every problem. Precise and every are very important qualifiers.
If you sacrifice precise and widen it to: "Halt" and "Maybe run forever, but might just take longer than the age of the universe and is thus irrelevant for actual programs we might choose to run" then it is decidable for every problem.
Every means that there exist programs, in the infinity of all programs, that can not be proven. It does not mean that no program can be proven. Programs that are 10^8000000 instructions long that are intentionally obfuscated count in every. Human-designed programs that humans want to be correct and are reasonably sure are correct are extremely well-behaved in comparison and their provable termination can almost always be reasoned about.
Generally speaking, human-designed programs are almost always implicitly being constructed in the space of programs that will terminate (possibly relative to a event loop). At every step of the process you only extend using provably terminating constructions. Few humans will have a loop condition like: "Terminates if the Goldbach Conjecture is true" which is one of those sorts of things that makes it hard to prove termination. Just stay away from unproven conjectures in your loop conditions and you will probably be fine.
WorldMaker 23 hours ago [-]
But again, the context is not about humans trying very hard to stick to problems in "terminating space" when writing software, but about LLMs with no such compunctions/boundaries finding inputs that break "terminating space assumptions". (Whether or not you also believe that LLMs are capable of staying within the lines of "terminating space" when generating code.)
Generally speaking, yes, humans want to design programs as best they can in the world of safely terminating applications. Humans aren't perfect at it today, given practical real world data such as CVE databases. Trying to hope humans become perfect to safeguard the world against LLMs like the Googler quote way above is the thing I find futile. Humans aren't going to magically get perfect. We need good enough solutions more than we need perfect solutions. The fear is that LLMs can greatly outpace humans in breaking "good enough" than humans can keep up in building "good enough".
Veserv 23 hours ago [-]
You can prove a program is correct and terminates for all inputs and, absent a hardware or other assumption vulnerability that breaks the abstract machine assumptions, there would be no inputs that "break" anything. In fact, almost any human-designed program that is correct and terminates would not just be provable, but "easy" to prove algorithmically (in the theoretical sense, in a practical sense existing techniques are insufficient to prove complex programs).
Even ignoring isolation guarantees that could generically prevent unbounded escalation for arbitrary programs, you can just reject anything that is not "easy" to prove. Humans are really dumb, so anything that is not directly proven or easy to prove automatically is almost certainly not correct, so you can just err on the safe side and just reject them if you care about global correctness.
buzzin__ 22 hours ago [-]
SolutionNotFound is a perfectly valid return case for my Algo. I start two threads, one searches for a solution, second one terminates the first after one second, if it is still running.
How in the world does the halting problem enters into the picture if my program is bug free or not?
mrkeen 6 hours ago [-]
The argument is that 'the program returns' is strictly easier to prove than 'the program returns the correct answer'. If the first is impossible, then the second is too.
I'm all in favour of sidestepping the argument by having our languages more resemble System F or some polymorphic lambda calculus.
WorldMaker 4 hours ago [-]
Though still useful to remember that some of the earliest mathematical write ups of the Halting Problem were also by Alonso Church and directly in the lambda calculus. The Church-Turing Theorem is a lasting reminder that the two worlds imperative and functional describe the same algorithms (form the set of Turing Completeness).
mrkeen 4 hours ago [-]
It depends on the type system you choose to apply to LC. Simply-typed LC terminates.
You have to include a construct that introduces general recursion to make it Turing complete.
There's a cool practical space within those constraints that needs more exploration.
Non-total functions can call total functions, but not vice-versa.
Imagine a web server whose main loop is non-total, because you want it to stay up. But each route is total, to guarantee termination.
ModernMech 1 days ago [-]
[dead]
kridsdale1 1 days ago [-]
Shhhhh!
It may be the only way to keep us all employed.
anigbrowl 1 days ago [-]
'Ruliology' is an ignorant neologism, and whoever thought it up should be dropped down a well. Canonology is linguistically consistent without being obscure.
layer8 1 days ago [-]
At least he isn’t abusing some existing term.
aaroninsf 1 days ago [-]
It's Wolfram-speak, so you'd want to drop Stephen if you're committed.
I didn't realize he'd coined it, but this is consistent. I don't want to drop him down a well because I think his ideas are very interesting, even if they're wrong. Nevertheless, [827 words deleted]!
kridsdale1 1 days ago [-]
I went through a process of “what the fuck is this bullshit” to “ok, yes, that makes sense and can suffice for my multiverse worldview until someone writes a better one” when I read all his foundational essays on the topic.
1 days ago [-]
crabbone 1 days ago [-]
> So let’s say you want to create a program that doesn’t have bugs. How should you do it? Fundamentally the only way to make sure a program will always do what you want is to understand everything it can do. But there’s a kind of paradox implicit in that: if you can really understand everything your program can do that basically means the program is doing something computationally reducible, and you probably in the end didn’t actually need to run the program with all its steps to get the result you wanted.
So... he has this "strange" idea of what makes a program useful... I wonder what does he think about a program that displays system time? Totally predictable! So, should it be just replaced by the output?
On a more serious note, at least from a perspective of a system programmer, vast majority of programs don't do (intentionally) this kind of nodeterministic stuff. They are more of a complex way of displaying information obtained by the sensors, or a way to cause the physical parts of the system to change their configuration. They are totally predictable, yet they still are absolutely necessary for the computer system to function.
codechicago277 1 days ago [-]
In this framing, clean coding abstractions gain a purpose beyond helping humans understand the code and actually help enforce that the end result is reasonably bug free. Building code out of understandable pieces can ensure that the whole thing is reasonably understandable.
While the article is focused on “low level” bugs, the key insight is that human understanding has limits, and bugs show up when the human is overconfident in their understanding, and unwilling to verify the code by running it on a sample of test cases. This does seem to help explain why “high level” bugs occur, where the reality somehow doesn’t match the assumption. Maybe a dependency is on the wrong version, a global variable isn’t initialized in certain cases, etc.
In a world of LLMs producing code that isn’t always understandable to humans, it does raise the question of how to enforce that AI code is bug free, and maybe forcing coding agents to stick to human abstractions is the missing piece.
Rendered at 21:23:02 GMT+0000 (Coordinated Universal Time) with Vercel.
You want a program that does X. So you think about what a program that does X should look like, and write a program that does what you think should produce result X, but maybe you made some mistakes.
but about the following, to my mind completely different, situation:
You want a program that does X. So you write a bunch of random short programs and after a while you find one that looks on small examples as if it's doing X. You use that one, but maybe actually it doesn't always work.
The key difference here is that in the first case you try to make there not be bugs by understanding what the program is doing and in the second you try to make there not be bugs by looking at the program's output.
(Perhaps some super-extreme practitioners of test-driven development might argue for something like the latter. Perhaps some AI-driven programming is uncomfortably close to it. But it's not, generally, how people have produced and debugged software.)
Wolfram kinda tries to justify this perspective by saying:
"Fundamentally the only way to make sure a program will always do what you want is to understand everything it can do. But there’s a kind of paradox implicit in that: if you can really understand everything your program can do that basically means the program is doing something computationally reducible, and you probably in the end didn’t actually need to run the program with all its steps to get the result you wanted."
but I think this is silly (and suspect it's the result of Wolfram trying to shoehorn his pet notion of "computational (ir)reducibility" into places where it brings no actual insight). It happens all the time that you write a program that (at least in principle) you understand completely, but that you don't know a much cheaper way to do it.
So they replace everything with extensional contexts, ie., in/out sets -- where things are replaceable by their values. And then use the machinery of very simple mathematics to analyse the situation.
In ML, consider comparing two classifiers extensionally, so that two classifiers "are the same" if they partition some input data exactly the same vs., declaring them different if they do so by means of some differing internal representation.
Since intensional contexts are the archetypal feature of mental representations, they're rarely analysed well by computer scientists.
I double checked it with ChatGPT if anyone is interested in more details: https://chatgpt.com/s/t_6a6883385ab481919126c7b631000815
And if you want additional assurance (due to, e.g. the computation being very long) you could probably use some cryptographic techniques to produce a certificate that the output is as it should be, and you can check that certificate as many times as you want to avoid possible random hardware errors in the process of checking the certificate.
I actually think criticism is especially important in the case of high-profile public figures like Wolfram. Far more people in the general public know about him and his highly speculative and unproven theories, while at the same time thousands of serious scientists publishing important and influential work go relatively unrecognized.
Here, before he starts, how do we know that the bugs in the Turing machine implementation of f(n)=n+1 are in any way representative of bugs in a normal computation? He seems to be generating random state machines and then evaluating them and picking ones which are nearly but not quite correct implementations of f(n)=n+1. Is that like a normal “honest” software bug? Is it like a deliberate software sabotage like you might look for when evaluating a software supply chain risk? Is it like the sort of vulnerability you might see when fuzzing? As far as I can see, there’s no reason to think it’s like any of these.
More broadly, since the “Principle of Computational Equivalence” and “computational irreducibility” are referred to as touchstones but are never actually defined or properly established how are we supposed to treat them? Interesting conjectures? Actual axioms? Something in between?
One thing I find tragic about Wolfram is that he found his holy grail, Rule 30, at the very beginning of his project and ever since he's found that every family of rules that he's look at that is sufficiently powerful has something like Rule 30 -- but always a bit more complex, complicated and not quite so beautiful, in fact often outright ugly...
... so he jumps into this sort of thing and samples of some of a ruliad, finds the usual things he finds in every ruliad, gets excited about it and thinks he has a "theory" and then moves on to something else and most of us are scratching our heads.
Whereas in stating the Principle of Computational Equivalence Wolfram says things like "... the evolution of weather systems can, in principle, compute the same things as a computer."[1]
Well, ... wtf? What does it mean to say the evolution of a weather system can compute something? Where do we even start on understanding this? I pick up a calculator and compute the volume of a cone. It's a sunny day outside. How do I "in principle" use that to check my calculation? It literally makes no sense whatsoever on its face as a claim but it is so slippery because of that "in principle" that it doesn't give me anything to hold onto that I could even test.
And that's before I even get started on the "underpants gnome" logical justification behind the claim, which seems to be:
1. Computers are complex
2. Weather is complex
3. Therefore they are "in some sense" equivalent
4. <don't worry about step 4>
5. Thus weather can "in principle" compute the same things as a computer.
I'm really not trying to misrepresent him, I'm just baffled.
[1] https://mathworld.wolfram.com/PrincipleofComputationalEquiva...
https://en.wikipedia.org/wiki/Chaos_computing
https://pubs.aip.org/aip/cha/article-abstract/35/9/093112/33...
For all I know, maybe he actually is the world-class genius he believes himself to be, but it's difficult to tell underneath all the blatant self-promotion.
After Quake was released and the principals of Id Software broke up, John Romero pretty much spent the next few years making an ass of himself during the development of Daikatana. When asked about the delayed and beleaguered development process on Slashdot, John Carmack kind of paid him a backhanded comment saying something like "A properly disciplined Romero is a credit to any team." And that's more or less what Wolfram is: properly disciplined, he would be an asset to any cutting-edge physics research team, but as he his he'd rather go down these rabbit holes than suffer to work with people of more ordinary intellect. And it's his, and the world's, loss really.
For me the ultimate proof that AI will have become super-intelligent is not that it will prove results that mathematicians can already deal with, it's that it will be able to look at a Turing machine and tell you "Yep, that's how it behaves, it follows these rules, and will never halt because this and that". I realize this is impossible in general, but if it's possible to some extent, where it is way better than the people over at busy beaver challenge, personally my mind will be blown.
https://youtu.be/B_7RpP90rUk (at 3:00)
But that doesn’t mean that it is impossible to have all our programs be formally verified. For that, if we have a formal specification for what each should do… Well, I suppose it’s possible that some program we would want is possible to implement with the desired properties, but not possible to prove that it has those properties? It is possible to enumerate (program, proof) pairs though.
Especially with the more recent relative of the Halting Problem combined with the Church-Turing Theorem that found mathematical proof of a "0-day" sandbox escape in the Universal Turing Machine itself.
We have always lived in a house of glass. LLM agents automating trebuchets for rock throwing certainly seems like a bad idea to me and "let's simply eliminate all software vulnerabilities" an interesting bit of ostrich work (stick your head in the sand and hope it all gets better).
No, the real issue is that for the most we don’t want to put the necessary effort into proving the relevant properties, because it’s costly and time-consuming, and we think we can live with the risk. The issue is not some theoretical inability to do so.
Potentially Infinite Loops are a great power. We've learned in most programming languages the "Uncle Ben lesson" that with such great power, comes great responsibility. In most programming languages we don't want to remove the ability to infinitely loop, because we might need that power, we work on ways to limit that responsibility (loop guards and timeouts and cancellations and teardowns). But it will likely always be possible to see some code spin in a loop we can't tell is accidentally infinite or just a loop with a lot more work than we expected. The infinite spin wait will always be a risk in our code.
I think it has a lot to do with the Halting Problem.
“We can’t write bug-free software due to the halting problem anyway” is an incorrect argument.
I don't know what properties you think people are trying to pragmatically prove about arbitrary programs but "did the program complete successfully" will always be an important, pragmatic property in software development. Especially in the pragmatic world where so much of our software is chaining smaller programs together to solve a task.
I'm saying we can't write perfectly bug-free software because of the Halting Problem and the inability to prove any given loop will not be infinite until running that loop. Perfect remains the enemy of the good and we certainly write a lot of "bug-free-enough" software without worrying about the Halting Problem day-to-day. But if you are saying the world needs to write perfectly bug free code starting tomorrow because LLMs will find all the vulnerabilities and sandbox escapes the Halting Problem is absolutely one of the reasons we can't ever provably hit that "perfect" target. We still need to find "good enough" or we give up on software development altogether and that's not what I'm advocating. Perfect is the enemy of the good. Mathematically perfect provably does not exist. Software will always have bugs, especially in the world with a threat model of active brute force machines.
You cannot find/prevent every case of an infinite loop at design time/compile time if the only way to determine a complex enough control flow converges towards halting is to run the full program in a live environment.
If you sacrifice precise and widen it to: "Halt" and "Maybe run forever, but might just take longer than the age of the universe and is thus irrelevant for actual programs we might choose to run" then it is decidable for every problem.
Every means that there exist programs, in the infinity of all programs, that can not be proven. It does not mean that no program can be proven. Programs that are 10^8000000 instructions long that are intentionally obfuscated count in every. Human-designed programs that humans want to be correct and are reasonably sure are correct are extremely well-behaved in comparison and their provable termination can almost always be reasoned about.
Generally speaking, human-designed programs are almost always implicitly being constructed in the space of programs that will terminate (possibly relative to a event loop). At every step of the process you only extend using provably terminating constructions. Few humans will have a loop condition like: "Terminates if the Goldbach Conjecture is true" which is one of those sorts of things that makes it hard to prove termination. Just stay away from unproven conjectures in your loop conditions and you will probably be fine.
Generally speaking, yes, humans want to design programs as best they can in the world of safely terminating applications. Humans aren't perfect at it today, given practical real world data such as CVE databases. Trying to hope humans become perfect to safeguard the world against LLMs like the Googler quote way above is the thing I find futile. Humans aren't going to magically get perfect. We need good enough solutions more than we need perfect solutions. The fear is that LLMs can greatly outpace humans in breaking "good enough" than humans can keep up in building "good enough".
Even ignoring isolation guarantees that could generically prevent unbounded escalation for arbitrary programs, you can just reject anything that is not "easy" to prove. Humans are really dumb, so anything that is not directly proven or easy to prove automatically is almost certainly not correct, so you can just err on the safe side and just reject them if you care about global correctness.
How in the world does the halting problem enters into the picture if my program is bug free or not?
I'm all in favour of sidestepping the argument by having our languages more resemble System F or some polymorphic lambda calculus.
You have to include a construct that introduces general recursion to make it Turing complete.
There's a cool practical space within those constraints that needs more exploration.
Non-total functions can call total functions, but not vice-versa.
Imagine a web server whose main loop is non-total, because you want it to stay up. But each route is total, to guarantee termination.
It may be the only way to keep us all employed.
It's part of his GUT. You will likely become committed to the well when you encounter ruliad: https://writings.stephenwolfram.com/2021/11/the-concept-of-t...
So... he has this "strange" idea of what makes a program useful... I wonder what does he think about a program that displays system time? Totally predictable! So, should it be just replaced by the output?
On a more serious note, at least from a perspective of a system programmer, vast majority of programs don't do (intentionally) this kind of nodeterministic stuff. They are more of a complex way of displaying information obtained by the sensors, or a way to cause the physical parts of the system to change their configuration. They are totally predictable, yet they still are absolutely necessary for the computer system to function.
While the article is focused on “low level” bugs, the key insight is that human understanding has limits, and bugs show up when the human is overconfident in their understanding, and unwilling to verify the code by running it on a sample of test cases. This does seem to help explain why “high level” bugs occur, where the reality somehow doesn’t match the assumption. Maybe a dependency is on the wrong version, a global variable isn’t initialized in certain cases, etc.
In a world of LLMs producing code that isn’t always understandable to humans, it does raise the question of how to enforce that AI code is bug free, and maybe forcing coding agents to stick to human abstractions is the missing piece.