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

Previous Next

Full log

Message #26 received at 38605 <at> debbugs.gnu.org (full text, mbox):

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

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

> Hi Simon,
>
> zimoun <zimon.toutoune <at> gmail.com> skribis:
>
>> To my knowledge, the most advanced ML-family language able to
>> bootstrap (and verified with prover etc.) is CakeML (subset of
>> Standard ML).
>>
>> (And not packaged in Guix, AFAICT.)
>>
>> https://cakeml.org/
>
> Right, thanks for the pointer!  CakeML is truly impressive.  It’s also
> nice to see how the tiny diagram to the right of the web page clearly
> and succinctly describes its compiler/language tower.
>
> Ludo’.

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
is where I think Amin Bandali (CC) and I's idea of writing a C-based
boostrapping compiler and dedicating it to the GNU project would be
really valuable.

Ultimately I think we need a vehicle for ML to be fledged out in Guix so
that we can have a consistent set of utilities for the formal methods
community to work in with Guix (see my formal methods working group
proposal email).

Maybe at some later date we could even fledge out that bootstrapping
compiler to be its own distinct implementation of ML, but i'll save that
for a later date. Regardless, the issue of binaries-on-binaries in ML
seems to be reaching back to 1993! It's about time we ended that. Stay
tuned for more information on what I think we could do about that.

-- 
Brett M. Gilio <brettg <at> posteo.net>
GNU Guix, Contributor <https://guix.gnu.org/>

Previous Next

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