[bug#38605] [WIP MLton 0/1] Add MLton

[Ludovic Courtès]

Hi,

zimoun <address@hidden> skribis:

> On Tue, 17 Dec 2019 at 03:21, Brett Gilio <address@hidden> 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’.