From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: =?utf-8?Q?=C3=93scar_Fuentes?= Newsgroups: gmane.emacs.devel Subject: Re: Have you all gone crazy? Was: On being web-friendly and why info must die Date: Fri, 19 Dec 2014 22:29:38 +0100 Message-ID: <8761d7ba65.fsf@wanadoo.es> 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: 8bit X-Trace: ger.gmane.org 1419024616 29451 80.91.229.3 (19 Dec 2014 21:30:16 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 19 Dec 2014 21:30:16 +0000 (UTC) To: emacs-devel@gnu.org Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Fri Dec 19 22:30:09 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 1Y257f-0007gK-RC for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 22:30:07 +0100 Original-Received: from localhost ([::1]:60606 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y257f-00086w-2q for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 16:30:07 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:42445) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y257W-00084H-Ud for emacs-devel@gnu.org; Fri, 19 Dec 2014 16:30:04 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1Y257R-0000YF-1D for emacs-devel@gnu.org; Fri, 19 Dec 2014 16:29:58 -0500 Original-Received: from plane.gmane.org ([80.91.229.3]:36933) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y257Q-0000Xn-RI for emacs-devel@gnu.org; Fri, 19 Dec 2014 16:29:52 -0500 Original-Received: from list by plane.gmane.org with local (Exim 4.69) (envelope-from ) id 1Y257O-0007YK-GT for emacs-devel@gnu.org; Fri, 19 Dec 2014 22:29:50 +0100 Original-Received: from 129.red-88-10-128.dynamicip.rima-tde.net ([88.10.128.129]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Fri, 19 Dec 2014 22:29:50 +0100 Original-Received: from ofv by 129.red-88-10-128.dynamicip.rima-tde.net with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Fri, 19 Dec 2014 22:29:50 +0100 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 16 Original-X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: 129.red-88-10-128.dynamicip.rima-tde.net User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.50 (gnu/linux) Cancel-Lock: sha1:V1hTH8d/+KYTLzIO30hHHw98e9E= X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 80.91.229.3 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:180352 Archived-At: Yuri Khan writes: > 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 “will terminate in ” is a > decidable property while “will terminate” is not. This is true if and only if you don't live in this universe. There is plenty of people who fits the bill, with Computer Scientists at the front row.