[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Brett Gilio
Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group
Date: Fri, 27 Dec 2019 20:55:00 -0600
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux)

Ludovic Courtès <address@hidden> writes:

> Hi!
> Julien Lepiller <address@hidden> 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]
<address@hidden> <address@hidden>

reply via email to

[Prev in Thread] Current Thread [Next in Thread]