From: "Ludovic Courtès" <ludo@gnu.org>
To: zimoun <zimon.toutoune@gmail.com>
Cc: Amin Bandali <bandali@gnu.org>, Brett Gilio <brettg@posteo.net>,
38605@debbugs.gnu.org
Subject: [bug#38605] [WIP MLton 0/1] Add MLton
Date: Wed, 18 Dec 2019 15:48:57 +0100 [thread overview]
Message-ID: <87zhfpofja.fsf@gnu.org> (raw)
In-Reply-To: <CAJ3okZ2MW3swvwLjZOJxRp8dFcjNEHvBVGwWdQaFeZT84250CA@mail.gmail.com> (zimoun's message of "Tue, 17 Dec 2019 17:42:51 +0100")
Hi,
zimoun <zimon.toutoune@gmail.com> skribis:
> On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg@posteo.net> 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. […] 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’ve been doing so
far. In essence, we’ve 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’t 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’.
next prev parent reply other threads:[~2019-12-18 14:50 UTC|newest]
Thread overview: 14+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-12-14 3:58 [bug#38605] [WIP MLton 0/1] Add MLton Brett Gilio
2019-12-14 3:59 ` [bug#38605] [WIP MLton 1/1] gnu: Add mlton Brett Gilio
2020-09-14 17:36 ` zimoun
2022-04-12 10:21 ` [bug#38605] [WIP MLton 0/1] Add MLton zimoun
2022-05-04 11:58 ` bug#38605: " zimoun
2019-12-14 17:58 ` [bug#38605] " Ludovic Courtès
2019-12-15 22:32 ` Brett Gilio
2019-12-16 10:02 ` Ludovic Courtès
2019-12-15 1:59 ` zimoun
2019-12-16 21:23 ` Ludovic Courtès
2019-12-17 2:20 ` Brett Gilio
2019-12-17 16:42 ` zimoun
2019-12-18 14:48 ` Ludovic Courtès [this message]
2019-12-21 4:56 ` Brett Gilio
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87zhfpofja.fsf@gnu.org \
--to=ludo@gnu.org \
--cc=38605@debbugs.gnu.org \
--cc=bandali@gnu.org \
--cc=brettg@posteo.net \
--cc=zimon.toutoune@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).