From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Hans Aberg Newsgroups: gmane.lisp.guile.user Subject: Re: A bit further toward the flamewar Date: Thu, 13 Oct 2011 23:58:23 +0200 Message-ID: References: <20111012153958.GA20242@ccellier.rd.securactive.lan> <87pqi2ca3q.fsf@gnu.org> <8739exry15.fsf@pobox.com> <20111013112709.GA28078@ccellier.rd.securactive.lan> <87r52hc6hu.fsf@gnu.org> <20111013185424.GA17999@yeeloong.happyleptic.org> <87d3e08uhy.fsf@gnu.org> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1318543119 9108 80.91.229.12 (13 Oct 2011 21:58:39 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 13 Oct 2011 21:58:39 +0000 (UTC) Cc: guile-user@gnu.org To: =?iso-8859-1?Q?Ludovic_Court=E8s?= Original-X-From: guile-user-bounces+guile-user=m.gmane.org@gnu.org Thu Oct 13 23:58:34 2011 Return-path: Envelope-to: guile-user@m.gmane.org Original-Received: from lists.gnu.org ([140.186.70.17]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1RETIO-0005RY-Ez for guile-user@m.gmane.org; Thu, 13 Oct 2011 23:58:32 +0200 Original-Received: from localhost ([::1]:55748 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1RETIO-0004Wm-1f for guile-user@m.gmane.org; Thu, 13 Oct 2011 17:58:32 -0400 Original-Received: from eggs.gnu.org ([140.186.70.92]:55525) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1RETIK-0004WT-5n for guile-user@gnu.org; Thu, 13 Oct 2011 17:58:29 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1RETIJ-0007Fw-DM for guile-user@gnu.org; Thu, 13 Oct 2011 17:58:28 -0400 Original-Received: from smtp-out21.han.skanova.net ([195.67.226.208]:48995) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1RETII-0007EU-6g; Thu, 13 Oct 2011 17:58:26 -0400 Original-Received: from [10.0.1.2] (217.210.127.13) by smtp-out21.han.skanova.net (8.5.133) (authenticated as u26619196) id 4E79D85B008CDD80; Thu, 13 Oct 2011 23:58:24 +0200 In-Reply-To: <87d3e08uhy.fsf@gnu.org> X-Mailer: Apple Mail (2.1084) X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 195.67.226.208 X-BeenThere: guile-user@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: General Guile related discussions List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-user-bounces+guile-user=m.gmane.org@gnu.org Original-Sender: guile-user-bounces+guile-user=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.user:8879 Archived-At: On 13 Oct 2011, at 23:14, Ludovic Court=E8s wrote: > Did you know that Coq would only compile a function when it can prove > that it terminates? That=92s another kind of compiler-supported proof = one > quickly gets used to. Termination is a non-deducable property. They look at a intuitionistic = subset of programs. Hans