From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Yuri Khan Newsgroups: gmane.emacs.devel Subject: Re: Have you all gone crazy? Was: On being web-friendly and why info must die Date: Sat, 20 Dec 2014 03:52:30 +0700 Message-ID: References: <87y4q69m4a.fsf@fencepost.gnu.org> <87mw6m9dt7.fsf@fencepost.gnu.org> <878ui3o06l.fsf@newcastle.ac.uk> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1419022364 26497 80.91.229.3 (19 Dec 2014 20:52:44 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 19 Dec 2014 20:52:44 +0000 (UTC) Cc: David Kastrup , emacs , Stefan Monnier , Sven Axelsson To: Phillip Lord Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Fri Dec 19 21:52:37 2014 Return-path: Envelope-to: ged-emacs-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Y24XN-000768-0E for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 21:52:37 +0100 Original-Received: from localhost ([::1]:60508 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24XM-0007WV-7w for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 15:52:36 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:35045) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24XJ-0007WH-Ha for emacs-devel@gnu.org; Fri, 19 Dec 2014 15:52:34 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1Y24XI-0002v2-MP for emacs-devel@gnu.org; Fri, 19 Dec 2014 15:52:33 -0500 Original-Received: from mail-ie0-x22b.google.com ([2607:f8b0:4001:c03::22b]:60802) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24XH-0002un-8u; Fri, 19 Dec 2014 15:52:31 -0500 Original-Received: by mail-ie0-f171.google.com with SMTP id ar1so1443263iec.16; Fri, 19 Dec 2014 12:52:30 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date:message-id:subject :from:to:cc:content-type:content-transfer-encoding; bh=XOnkVDazRpyzmxgeXnmzn7vfHng5B1bKg5C85Jmrty8=; b=HX9/a0AO6TxGB3O6yJJWFwNp0yeGdarZGJSEJOes0wTHDd6ESmxhwZKc9Ndo0oI4Xw DyYwL5jdlVkBx5WIH50jiwJUFdbPbHkBcJ4hKNNRYrqCCqVstK6S0nZyzIybA05k6lBj iUNCyREWoItsSKXXvz46D9IKzUTsWZ+LLRdlwqaIqLNzXDp9KitQgqzr5SzihwFfQVQn qv9mRJ7m0Ud567P/77JRdfNm+4C5hHt7xeFJNaYXFfcVhHsobHx9vrSgArI+zrWfS65Y x4KU7IkgApWE9Z5B0Ijxz4l69pHmQ8NFrdzrg+KHUkbrFlEx2Yqtec1im7f4pId9mWoc SWVg== X-Received: by 10.107.152.144 with SMTP id a138mr9633105ioe.39.1419022350585; Fri, 19 Dec 2014 12:52:30 -0800 (PST) Original-Received: by 10.107.48.82 with HTTP; Fri, 19 Dec 2014 12:52:30 -0800 (PST) In-Reply-To: <878ui3o06l.fsf@newcastle.ac.uk> X-Google-Sender-Auth: Scteb2desQZcpGXZxGFjl2LaNGI X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address (bad octet value). X-Received-From: 2607:f8b0:4001:c03::22b X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Original-Sender: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.devel:180349 Archived-At: On Sat, Dec 20, 2014 at 2:26 AM, Phillip Lord wrote: > Sadly this requires proof checkers that can distinguish between "will > terminate" and "will terminate within the known life-time of the > universe". That's a research problem I fear. Actually =E2=80=9Cwill terminate in =E2=80= =9D is a decidable property while =E2=80=9Cwill terminate=E2=80=9D is not. Although, in general, the finite-interval-termination problem is solved by setting up a timer watchdog and running the subject program. If it finishes first, then return t; if the watchdog barks first, then kill the program and return nil.