From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:39108) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iiWp5-0003Qe-MT for guix-patches@gnu.org; Fri, 20 Dec 2019 23:57:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iiWp4-00088e-E7 for guix-patches@gnu.org; Fri, 20 Dec 2019 23:57:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:41545) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iiWp4-00087u-7V for guix-patches@gnu.org; Fri, 20 Dec 2019 23:57:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iiWp4-0002ml-6x for guix-patches@gnu.org; Fri, 20 Dec 2019 23:57:02 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: From: Brett Gilio References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> <87k16wdkx0.fsf@gnu.org> <878snbzo8y.fsf@posteo.net> <87zhfpofja.fsf@gnu.org> Date: Fri, 20 Dec 2019 22:56:24 -0600 In-Reply-To: <87zhfpofja.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Wed, 18 Dec 2019 15:48:57 +0100") Message-ID: <87a77mqnt3.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Ludovic =?UTF-8?Q?Court=C3=A8s?= Cc: Brett Gilio , 38605@debbugs.gnu.org, Amin Bandali , zimoun Ludovic Court=C3=A8s writes: > Hi, > > zimoun skribis: > >> On Tue, 17 Dec 2019 at 03:21, Brett Gilio wrote: >> >>> I may be misspeaking, but I think CakeML is formally verified in HOL >>> which bootstraps against PolyML or SMLnj, and also requires MLton. So >>> the issue of cyclic binary-derived bootstrapping remains an issue. This >> >> I have not checked myself and if I understand well your point: CakeML >> requires one PolyML binary to bootstrap (see Bootstrapping locally in >> [1] which points to [2]). And this PolyML binary is not small and >> requires other not-so-small binaries to be produced. And I am not >> talking about the HOL part. So their claim that CakeML bootstraps >> really depends on how is defined "bootstrap". :-) > > Their claim is summarized on the home page (emphasis mine): > > The CakeML compiler has been bootstrapped inside HOL. By bootstrapped > we mean that the compiler has compiled itself. [=E2=80=A6] The result i= s a > verified binary that _provably_ implements the compiler itself > > IOW, their approach is to provide a formal proof that a given byte > stream corresponds to the given source code. > > This approach is very different from everything we=E2=80=99ve been doing = so > far. In essence, we=E2=80=99ve been focusing on building everything from > source, with the assumption that source code is auditable. > > Instead of doing that, they formally provide the source/binary > correspondence, which is much stronger. Once you have this proof, it > doesn=E2=80=99t matter how HOL or PolyML or any other dependency is built= , AIUI. > > In theory, HOL could be the target of a trusting-trust attack. But then > again, one could very well check it with paper-and-pen or with HOL plus > manual verification. > > Food for thought! > > Ludo=E2=80=99. > > > > I kind of wonder if their method of having a HOL-implemented proof for their source/binary bytestream is a possibility for GNU Guix in the future? It makes for an interesting speculation, especially for system-level proofs of blob trust. Bandli? --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]