From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: ludo@gnu.org (Ludovic =?iso-8859-1?Q?Court=E8s?=) Newsgroups: gmane.lisp.guile.user Subject: Re: A bit further toward the flamewar Date: Thu, 13 Oct 2011 19:43:48 +0200 Message-ID: <874nzcdbxn.fsf@gnu.org> 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> <87r52grk90.fsf@pobox.com> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1318527843 31643 80.91.229.12 (13 Oct 2011 17:44:03 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 13 Oct 2011 17:44:03 +0000 (UTC) Cc: guile-user@gnu.org To: Andy Wingo Original-X-From: guile-user-bounces+guile-user=m.gmane.org@gnu.org Thu Oct 13 19:43:59 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 1REPK1-0000yg-Lq for guile-user@m.gmane.org; Thu, 13 Oct 2011 19:43:57 +0200 Original-Received: from localhost ([::1]:33247 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1REPK1-0003zG-2j for guile-user@m.gmane.org; Thu, 13 Oct 2011 13:43:57 -0400 Original-Received: from eggs.gnu.org ([140.186.70.92]:56989) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1REPJw-0003yz-Vr for guile-user@gnu.org; Thu, 13 Oct 2011 13:43:53 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1REPJv-000458-Ux for guile-user@gnu.org; Thu, 13 Oct 2011 13:43:52 -0400 Original-Received: from mail1-relais-roc.national.inria.fr ([192.134.164.82]:5877) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1REPJv-000452-PF for guile-user@gnu.org; Thu, 13 Oct 2011 13:43:51 -0400 X-IronPort-AV: E=Sophos;i="4.69,341,1315173600"; d="scan'208";a="124020455" Original-Received: from reverse-83.fdn.fr (HELO pluto) ([80.67.176.83]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 13 Oct 2011 19:43:49 +0200 X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 22 =?iso-8859-1?Q?Vend=E9miaire?= an 220 de la =?iso-8859-1?Q?R=E9volution?= X-PGP-Key-ID: 0xEA52ECF4 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 83C4 F8E5 10A3 3B4C 5BEA D15D 77DD 95E2 EA52 ECF4 X-OS: x86_64-unknown-linux-gnu In-Reply-To: <87r52grk90.fsf@pobox.com> (Andy Wingo's message of "Thu, 13 Oct 2011 17:20:27 +0200") User-Agent: Gnus/5.110018 (No Gnus v0.18) Emacs/24.0.90 (gnu/linux) X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 192.134.164.82 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:8872 Archived-At: Hello! Andy Wingo skribis: > Anyway this second, proof side of types, is the side that Scheme does > not have. C has a stronger story in that regard. Right; but let=E2=80=99s not oversell C. ;-) Lisps are definitely closer = to automated theorem provers than C. ACL2 and =CE=B1leanTAP come to mind. Ludo=E2=80=99.