From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Richard Stallman Newsgroups: gmane.lisp.guile.devel,gmane.comp.gnu.lightning.general Subject: Re: Reinterpreting the compiler source code Date: Sat, 06 Sep 2014 18:16:43 -0400 Message-ID: References: Reply-To: rms@gnu.org NNTP-Posting-Host: plane.gmane.org Content-Type: text/plain; charset=ISO-8859-15 X-Trace: ger.gmane.org 1410041816 6016 80.91.229.3 (6 Sep 2014 22:16:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 6 Sep 2014 22:16:56 +0000 (UTC) Cc: torvalds@osdl.org, lightning@gnu.org, deraadt@theos.com, Markus.Kuhn@cl.cam.ac.uk, guile-devel@gnu.org To: Ian Grant Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Sun Sep 07 00:16:51 2014 Return-path: Envelope-to: guile-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 1XQOHq-0000dL-5q for guile-devel@m.gmane.org; Sun, 07 Sep 2014 00:16:50 +0200 Original-Received: from localhost ([::1]:36392 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQOHp-00061A-CE for guile-devel@m.gmane.org; Sat, 06 Sep 2014 18:16:49 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:47845) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQOHm-000614-JC for guile-devel@gnu.org; Sat, 06 Sep 2014 18:16:47 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XQOHl-0002Fj-A3 for guile-devel@gnu.org; Sat, 06 Sep 2014 18:16:46 -0400 Original-Received: from fencepost.gnu.org ([2001:4830:134:3::e]:41708) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQOHl-0002Ff-6c; Sat, 06 Sep 2014 18:16:45 -0400 Original-Received: from rms by fencepost.gnu.org with local (Exim 4.71) (envelope-from ) id 1XQOHj-0006L5-Oz; Sat, 06 Sep 2014 18:16:43 -0400 In-reply-to: (message from Ian Grant on Thu, 4 Sep 2014 22:23:41 -0400) X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address (bad octet value). X-Received-From: 2001:4830:134:3::e X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:17424 gmane.comp.gnu.lightning.general:576 Archived-At: [[[ To any NSA and FBI agents reading my email: please consider ]]] [[[ whether defending the US Constitution against all enemies, ]]] [[[ foreign or domestic, requires you to follow Snowden's example. ]]] I can speak in favor of any serious effort to try to verify that our binaries match our souce code. > What we need is a language with a simple semantics for which we can write > interpreters from scratch. It will be slow, but that doesn't matter. All we > need it for is to generate the reference compiler that we know is secure, > and the reference tools that we use to verify that the object code produced > by the full 740 MB of GCC source when compiled by the 74MB gcc binaries, is > the same object code our reference compiler produces. I did not understand, until now, that this was meant as a way to verify GCC. I thought you meant we should stop using our existing tools and program in this language instead. I was not interested in that. However, as a scheme to verify our tools and keep using them, it might make sense. I can't judge how effective this sort of proof might be, but I won't reject the idea. -- Dr Richard Stallman President, Free Software Foundation 51 Franklin St Boston MA 02110 USA www.fsf.org www.gnu.org Skype: No way! That's nonfree (freedom-denying) software. Use Ekiga or an ordinary phone call.