GNU bug report logs - #38605
[WIP MLton 0/1] Add MLton

Previous Next

Full log

View this message in rfc822 format

From: Brett Gilio <brettg <at> gnu.org>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: Brett Gilio <brettg <at> posteo.net>, 38605 <at> debbugs.gnu.org, Amin Bandali <bandali <at> gnu.org>, zimoun <zimon.toutoune <at> gmail.com>
Subject: [bug#38605] [WIP MLton 0/1] Add MLton
Date: Fri, 20 Dec 2019 22:56:24 -0600

Ludovic Courtès <ludo <at> gnu.org> writes:

> Hi,
>
> zimoun <zimon.toutoune <at> gmail.com> skribis:
>
>> On Tue, 17 Dec 2019 at 03:21, Brett Gilio <brettg <at> 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’.
>
>
>
>

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?

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg <at> gnu.org> <brettg <at> posteo.net>

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.