From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Ian Grant Newsgroups: gmane.comp.gnu.lightning.general,gmane.lisp.guile.devel Subject: Re: GNU Thunder Date: Mon, 25 Aug 2014 16:59:32 -0400 Message-ID: References: NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============2378143210197537342==" X-Trace: ger.gmane.org 1409000385 18017 80.91.229.3 (25 Aug 2014 20:59:45 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 25 Aug 2014 20:59:45 +0000 (UTC) To: Richard Stallman , guile-devel-mXXj517/zsQ@public.gmane.org, lightning Original-X-From: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Mon Aug 25 22:59:41 2014 Return-path: Envelope-to: gcglg-lightning@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 1XM1Ma-0002Gu-Ld for gcglg-lightning@m.gmane.org; Mon, 25 Aug 2014 22:59:40 +0200 Original-Received: from localhost ([::1]:50534 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XM1Ma-0004Ud-B7 for gcglg-lightning@m.gmane.org; Mon, 25 Aug 2014 16:59:40 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:40489) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XM1MV-0004UW-IY for lightning-mXXj517/zsQ@public.gmane.org; Mon, 25 Aug 2014 16:59:36 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XM1MU-0008O1-15 for lightning-mXXj517/zsQ@public.gmane.org; Mon, 25 Aug 2014 16:59:35 -0400 Original-Received: from mail-wg0-x229.google.com ([2a00:1450:400c:c00::229]:43141) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XM1MT-0008Nt-LT; Mon, 25 Aug 2014 16:59:33 -0400 Original-Received: by mail-wg0-f41.google.com with SMTP id z12so13516746wgg.0 for ; Mon, 25 Aug 2014 13:59:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; bh=RVoQ2dZufmtnusXsKhiEHxZMzIH8bEJglqp6WW4vePo=; b=P7QBUjAeW6CHRziZvYcfc76bpwXXyPMfxH+Mha6TbZ+sLlMSfcb+8xsYg/VVn1/391 txyyJXu/hKWyMWJHQldL05Hk5MnOLejTpWJ6QLXooQj++MrVYc72umOnImcas/gIggXV upTsG3H38TCWC+2qDjRQrjvE7dFGNHYOOqByWBDpwd/0Gs78N9epOnCOfbgSBLEtUc0Y Va/YnKOTqqT1oWoOFi/RExL+a3O3V31TzCtF52zQFfySPkKufBk6YK00kDQOZdkBMFhV ODpX/eYcxevxiRDf6763Yx88kBEsNhAQE0zV1hAn9BmH8jo8M/7RisKbJU5x2DcRzFOh nLmQ== X-Received: by 10.180.184.99 with SMTP id et3mr17901933wic.31.1409000372431; Mon, 25 Aug 2014 13:59:32 -0700 (PDT) Original-Received: by 10.194.219.234 with HTTP; Mon, 25 Aug 2014 13:59:32 -0700 (PDT) In-Reply-To: X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address (bad octet value). X-Received-From: 2a00:1450:400c:c00::229 X-BeenThere: lightning-mXXj517/zsQ@public.gmane.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Original-Sender: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Xref: news.gmane.org gmane.comp.gnu.lightning.general:544 gmane.lisp.guile.devel:17365 Archived-At: --===============2378143210197537342== Content-Type: multipart/alternative; boundary=001a11c2259eaff1d405017a768e --001a11c2259eaff1d405017a768e Content-Type: text/plain; charset=UTF-8 On Sun, Aug 24, 2014 at 12:07 AM, Richard Stallman wrote: > The research is all done. We just need to implement it. > > I would describe this as a domain for research, because it is > far from clear whether it could possibly work in practice; > if it could, it is not obvious how to make it work. > > It's not like writing an assembler, where we know it can work. We don't actually know the assembler _does_ work. That's what I tried to say. I didn't want to over-emphasise it, because I thought people might already be bored of me banging on about it But apparently not! The problem is the semantics of the whole GNU toolchain are inaccessible because they depend 100% on the proprietary non-free tools that were used to build them. This is important, so let me make a statement: There is not one single line of GNU source code, the meaning of which does not depend entirely on non-free proprietary software. The source code will not tell you what the software actually does. See Thompson's 1984 Turing Award Speech http://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf for the details. I quote: "The moral is obvious. You can't trust code that you did not totally create yourself. (Especially code from companies that employ people like me.) " He works for Google now, doesn't he :-) The trick Thompson demonstrates is what I call a _syntactic fixed-point_. He basically makes a Y combinator of the C compiler, so that it takes in its own source and outputs it again, but that does not mean that the source it outputs is the source you read when you look at the source-distribution. The solution is to establish a _semantic_ fixedpoint. But to do that we need to be able to generate arbitrarily many essentially different working implementations of the compiler, and make sure that the code it generates when it compiles itself is the same, whatever the particular implementation. So if we see that the version that we compiled into MS Word BASIC produces the same binary executable as the JavaScript and COBOL versions then we can have some more confidence that the semantics of the GNU toolchain haven't been hijacked, ... yet. Ian --001a11c2259eaff1d405017a768e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On Sun, Aug 24, 2014 at 12:07 AM, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org= > wrote:
=C2=A0
=C2=A0 =C2=A0= The research is all done. We just need to implement it.

I would describe this as a domain for research, because it is
far from clear whether it could possibly work in practice;
if it could, it is not obvious how to make it work.

It's not like writing an assembler, where we know it can work.
We don't actually know the ass= embler _does_ work. That's what I tried to say. I didn't want to ov= er-emphasise it, because I thought people might already be bored of me bang= ing on about it But apparently not! The problem is the semantics of the who= le GNU toolchain are inaccessible because they depend 100% on the proprieta= ry non-free tools that were used to build them.

This is important, so let me make a statement:

=C2=A0=C2=A0=C2= =A0=C2=A0 There is not one single line of GNU source code, the meaning
= =C2=A0 =C2=A0 =C2=A0 of which does not depend entirely on non-free propriet= ary
=C2=A0 =C2=A0 =C2=A0 software.

The source code will not tell you what the softw= are actually does. See Thompson's 1984 Turing Award Speech http://w= ww.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf for the deta= ils. I quote:

=C2=A0=C2=A0=C2=A0=C2=A0 "The moral is obvious. You can't trus= t code that you did not
=C2=A0 =C2=A0 =C2=A0=C2=A0 totally create yourse= lf. (Especially code from companies
=C2=A0 =C2=A0 =C2=A0=C2=A0 that empl= oy people like me.) "

He works for Google now, doesn't he :-)

The trick Thompson demonstrates is what I call a _syntactic fixed-= point_. He basically makes a Y combinator of the C compiler, so that it tak= es in its own source and outputs it again, but that does not mean that the = source it outputs is the source you read when you look at the source-distri= bution.

The solution is to establish a _semant= ic_ fixedpoint. But to do that we need to be able to generate arbitrarily m= any essentially different working implementations of the compiler, and make= sure that the code it generates when it compiles itself is the same, whate= ver the particular implementation. So if we see that the version that we co= mpiled into MS Word BASIC produces the same binary executable as the JavaSc= ript and COBOL versions then we can have some more confidence that the sema= ntics of the GNU toolchain haven't been hijacked, ... yet.

Ian



--001a11c2259eaff1d405017a768e-- --===============2378143210197537342== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline _______________________________________________ Lightning mailing list Lightning-mXXj517/zsQ@public.gmane.org https://lists.gnu.org/mailman/listinfo/lightning --===============2378143210197537342==--