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

[Brett Gilio <brettg@posteo.net>]

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

> Hi Simon,
>
> zimoun <zimon.toutoune@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@posteo.net>
GNU Guix, Contributor <https://guix.gnu.org/>