Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Towards a Theory of Bugs: The Ruliology of the Unexpected

writings.stephenwolfram.com

Post reply on HN
Print view View original

21–30 of 51 posts

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#21

Post by layer8 »

WorldMaker wrote: post #20
layer8 wrote: post #18

Earlier quoted context omitted.

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.…

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 enou…

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.

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#22

Post by ModernMech »

WorldMaker wrote: post #20
layer8 wrote: post #18

Earlier quoted context omitted.

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.…

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 enou…

[dead]

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#23

Post by WorldMaker »

layer8 wrote: post #21
WorldMaker wrote: post #20

Earlier quoted context omitted.

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 enou…

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…

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.

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#24

Post by marssaxman »

seanhunter wrote: post #6

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 genera…

[flagged]

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#25

Post by o_nate »

gjm11 wrote: post #4

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 prog…

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.

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#27

Post by crabbone »

> 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.

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#28

Post by voidmain »

WorldMaker wrote: post #23
layer8 wrote: post #21

Earlier quoted context omitted.

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…

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 toge…

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!

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#29

Post by Veserv »

WorldMaker wrote: post #23
layer8 wrote: post #21

Earlier quoted context omitted.

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…

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 toge…

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.

Re: Towards a Theory of Bugs: The Ruliology of the Unexpected

#30

Post by sha16384 »

marssaxman wrote: post #24
seanhunter wrote: post #6

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 genera…

[flagged]

Isn't that also the point of your comment only much lazier?
Post reply on HN