I thought the message at the end about people expecting full correctness was a bit off; after all, if we expected fully-correct programs, we would be proving them instead of writing C.
MIT develops new tool that can interrupt infinite loops
61–70 of 72 posts
Re: MIT develops new tool that can interrupt infinite loops
#62Earlier quoted context omitted.
i wish i could do that for safari
You probably can: $ gdb /Applications/Safari.app/Contents/MacOS/Safari $PID iTunes, annoyingly, uses Apple's stupid little "please don't ptrace me" flag, which is a minor inconvenience, but fairly readily circumventable.
Sorry, couldn't resist.
Re: MIT develops new tool that can interrupt infinite loops
#63Re: MIT develops new tool that can interrupt infinite loops
#64Earlier quoted context omitted.
i wish i could do that for safari
You probably can: $ gdb /Applications/Safari.app/Contents/MacOS/Safari $PID iTunes, annoyingly, uses Apple's stupid little "please don't ptrace me" flag, which is a minor inconvenience, but fairly readily circumventable.
Re: MIT develops new tool that can interrupt infinite loops
#65Earlier quoted context omitted.
Why would that be bounded far below modern memory limits? Why would that be bounded at all ? Secondly, you're making the logic error A => B implies not A => not B. If state spaces as large as modern memory limits allow are too large, that doesn't imply that state spaces far below modern memory limits are small enough to handle. Thirdly, your program trivially terminates doing nothing.
Troll-feeding time! Pretend that an OOM condition is the same as a False answer. :3 Here's a program, building on the previous one, which either terminates or doesn't. from itertools import count for i in count(1): if not is_collatz(i): break
Real-life computers have bounded memory, so they don't have any more computational power than, say, regular expressions matchers -- every computational task performed by real computer can be represented by appropriately complicated regular expression. That's why one needs to be especially careful when arguing from computability when talking about real-life problems.
The more serious issue is a treatment of I/O.
Re: MIT develops new tool that can interrupt infinite loops
#66Earlier quoted context omitted.
Due to the fact that a program is a composition of programs which at the lowest level are loops and instructions this also means that it is impossible to determine whether or not a loop halts. It is easily provable that this is theoretically possible, but the required time is too long for it to be applicable. Suppose your memory has N states. Run your program through N+1 computation steps and if it's not already fini…
It also may not be applicable if you don't actually have access to all memory states involved. E.g. when communicating with a 3rd party computer over a network.
Let's consider both computers (yours and 3rd party) as a single computational device, with a state represented by a pair of symbols, where the first represents your computer and the second the 3rd party's. Suppose your computer has N states and the other M. It's enough to run N * M + 1 computation steps -- if your program hasn't ended so far, it will never, for there's a certain state (a, b) that must have occured twice, by the pigeonhole principle.
Please keep in mind that this is all purely theoretical, and not at all practical. It's just a counterargument to other purely theoretical argument from unsolvability of halting problem.
Re: MIT develops new tool that can interrupt infinite loops
#67Earlier quoted context omitted.
Thanks for the explanation! No shame here (I didn't study CS in undergrad) but I find it intuitive that a program can't detect an input that would loop indefinitely.
If that's intuitive for you already (great!) consider one step further: Rice's Theorem. Rice's Theorem in layman's term is "all nontrivial properties of a program are undecidable in the general case". "Undecidable" is the difficulty class of the halting problem (there are actually harder problems!). A couple accessible examples: 1. Constant Propagation - we know that we'll never detect all compile-time constants beca…
Re: MIT develops new tool that can interrupt infinite loops
#68This is a good line of investigation. I don't understand all the harrumphing here, except possibly as a means of self-congratulations at to why the harrumpher in question didn't bother inventing this tool themselves and how they understand the "halting problem" in a way not known at MIT. As the economist famously joked in response to 'how are you'... "Compared to what?" The comparison here is to killing the program a…
Most of the comments here are pretty fair about where Jolt might not be applicable (busy loops) and how this approach could be integrated with development; we touch on many these points in the paper (already linked by someone in the comments).
All of our emails are on the interwebs, so feel free to ping us if you want more information.
Re: MIT develops new tool that can interrupt infinite loops
#69This is a good line of investigation. I don't understand all the harrumphing here, except possibly as a means of self-congratulations at to why the harrumpher in question didn't bother inventing this tool themselves and how they understand the "halting problem" in a way not known at MIT. As the economist famously joked in response to 'how are you'... "Compared to what?" The comparison here is to killing the program a…
Re: MIT develops new tool that can interrupt infinite loops
#70What if you wrote an infinite loop, and wanted it that way? There are plenty of legitimate uses for an infinite loop, a REPL, a server, etc.