On Jan 28, 2008 2:08 PM, Bob Mottram <[EMAIL PROTECTED]> wrote: > On 28/01/2008, Vladimir Nesov <[EMAIL PROTECTED]> wrote: > > You can try checking out for example this paper (link from LtU > > discussion), which presents a rather powerful language for describing > > terminating programs: > > http://lambda-the-ultimate.org/node/2003 > > Also see http://en.wikipedia.org/wiki/Total_functional_programming > > This seems to address the halting problem by ignoring it (the same > approach researchers often take to difficult problems in computer > vision).
Well, what's pejorative with these solutions? You don't really need to write bad programs, so problem of checking if program is bad is void if you have a method for writing programs that are guaranteed to be good. > For practical purposes timeouts or watchdogs are ok, but > they're just engineering workarounds rather than solutions. In > practice biological intelligence also uses the same hacks, and I think > Turing himself pointed this out. Timeout is a trivial answer for a theoretical question, whereas type systems allow writing normal code without 'hacks' that also has these properties. But it's not practically feasible to use them currently, you'll spend too much time proving that program is correct and too little time actually writing it. Maybe in time tools will catch up... -- Vladimir Nesov mailto:[EMAIL PROTECTED] ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=90503888-2fa9e5
