From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:35111) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ihaeJ-00073J-UI for guix-patches@gnu.org; Wed, 18 Dec 2019 09:50:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ihaeI-0008Bt-PA for guix-patches@gnu.org; Wed, 18 Dec 2019 09:50:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:36841) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ihaeI-0008Ao-JO for guix-patches@gnu.org; Wed, 18 Dec 2019 09:50:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ihaeI-0003Bf-Gi for guix-patches@gnu.org; Wed, 18 Dec 2019 09:50:02 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: From: Ludovic =?UTF-8?Q?Court=C3=A8s?= 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> Date: Wed, 18 Dec 2019 15:48:57 +0100 In-Reply-To: (zimoun's message of "Tue, 17 Dec 2019 17:42:51 +0100") Message-ID: <87zhfpofja.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: zimoun Cc: Amin Bandali , Brett Gilio , 38605@debbugs.gnu.org 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 is 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.