Re: [Proposal] The Formal Methods in GNU Guix Working Group

[Brett Gilio <brettg@gnu.org>]

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

> Hi!
>
> Julien Lepiller <julien@lepiller.eu> skribis:
>
>> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
>> itself (using a bootstrapped bytecode interpreter written in C) to
>> build itself. Fortunately this situation is being worked on by a phd
>> student of Xavier Leroy (and nixOS user) :).
>>
>> The plan is to write a compiler in C or Scheme (it currently exists,
>> but is written in OCaml) for "miniML" a small subset of the OCaml
>> language. Then, there is already an interpreter in miniML able to
>> interpret the OCaml compiler compiling itself. Once the miniML
>> compiler is bootstrapped, we will have a path from C to OCaml :)
>
> Do you have pointers to this work?
>
> Hannes of MirageOS also mentioned it at the Reproducible Builds Summit.
> It sounds exciting!
>
> Ludo’.
>

I am also interested in this. MirageOS has a long lineage of making
sensible decisions in their development aside from just designing their
unikernel. So i'd really like to see if this becomes a possible bridge
from C or Scheme to a bootstrappable OCaml. For what I wonder, I think
this is something a formal methods community in Guix would be able to
contribute to so we see to it that GNU Guix has a good foundation for
making OCaml properly bootstrappable.

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