News for hackers. Stuff that matters.
Re:Gödel Without (Too Many) Tears by jerf on Monday September 30, 2013 @03:49PM (#6471874)
It's easier to answer that question about the Halting Problem, so here's Scott Aaronson proving it as a corollary to the Halting Problem: http://www.scottaaronson.com/blog/?p=710

Then, defending the value of the Halting Problem as a real problem is easy, relatively generally through Rice's Theorem: http://en.wikipedia.org/wiki/Rice%27s_theorem

In colloquial terms, one can render Rice's Theorem as "Would you like to produce a program that can prove anything remotely interesting across the set of all possible inputs? TOO BAD!" That's glib, but less inaccurate than we'd like.

Godel's theorem is, as Scott said, really sort of ad hoc and hard to easily apply in your head the way you're asking about. The Halting Problem, on the other hand, turns up everywhere, in real life (though many people still often don't realize it).

Re:Gödel Without (Too Many) Tears by PeterisP on Monday September 30, 2013 @06:37PM (#6472833)
My personal pet peeve is the Halting problem - yes, we can't prove interesting things for 'set of all possible inputs'.

However, my [unverified] gut feeling is that we can prove halting/nonhalting (via static analysis and restricting types of code that are allowed) for the large class of things that we actually use (or should use) in practice and vice versa - we should push the convoluted cases (where analysis isn't possible) away from practical usage, since if a well-designed computer system can't reason about them, then likely the programmer can't as well and that part is buggy in some corner case.

I.e., if your webservice isn't provably halting, guaranteeing a return value within a (short) bounded time - then it's too complex and is 99.9% likely to have a security flaw that allows denial of service or execution of arbitrary code in which case, naturally, you can't reason about it as the halting theorem proves.

We don't even need to know a "proper" answer to the halting question - guaranteed to finish under X steps/whatever: okay; not guaranteed (maybe halting in X+1 steps): suspect/bad. That would be good enough for practical purposes in most systems.

Re:Gödel Without (Too Many) Tears by jerf on Monday September 30, 2013 @10:28PM (#6473669)
It is unclear to me whether you are advocating for a programming style that you think is desirable but nonexistent, or if you're advocating for a programming style without naming it.

If the former, you should know you are not alone and serious attempts to create such programming languages are afoot. It's hard for me to find any solid, single web page to point you at, but you want to look at the more theoretical end of Haskell, and Agda and Coq, for some examples. Interesting Google terms include "structural recursion" and various other recursion schemes, and also things like http://blog.sigfpe.com/2007/07/data-and-codata.html .

Re:Gödel Without (Too Many) Tears by munin on Monday September 30, 2013 @07:03PM (#6472936)
you're right.

you can also soundly construct an analysis that asks "is this program safe" and answers with one of {yes, no, maybe I don't know}. and then, you interpret a result of "no" and "maybe I don't know" to mean the same thing and re-write the program until you get a "yes"...

Re:Gödel Without (Too Many) Tears by ElectroPrime on Monday September 30, 2013 @09:45PM (#6473556)
Keep in mind that real world computers just have a very large (but not unbounded) amount of tape. Since they have constant space, they are really just DFAs.
Re:Gödel Without (Too Many) Tears by jronkone on Tuesday October 01, 2013 @12:54AM (#6474145)
Does taking input from the outside (e.g. internet) change this?