[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: zimoun
Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group
Date: Mon, 16 Dec 2019 20:46:28 +0100


I am not a Programming Language Theory guy so I speak as a pure noob. :-)
Well, I am working in University Paris 7 Diderot doing some scientific

On Mon, 16 Dec 2019 at 02:00, Brett Gilio <address@hidden> wrote:

> so this could be more of a chance to see bigger institutions begin to
> adopt Guix for their research work.

IMHO, today the "win" is not about bootstrapping because it is
strongly language dependent but this "win" offered by Guix is about
the time-traveling reproducibility tools: today the key point in
scientific research (IMHO).
And yes, the reproducibility over the time means bootstrappability.
But it is each scientific community that must take care of its

The wider adoption could come from features as "time-machine",
available packages (channels for the not GNU compliant), easy to
distribute, to reproduce, be able to search in all the packages over
all the Guix history, etc.

And what I see as a blocking wider adoption by the Researcher around
me is: Mac. A lot of them just use Mac, I mean they develop daily on
MacOS and then once it is ready run on linux HPC clusters.

I know the article by Ludo and Ricardo. :-) And I strongly agree.
>From my point of view, the only way to attract more researchers is to
have an half-baked Guix working on Mac, IMHO.

> -- A lot of proof assistants are based on dialects of ML. Most of these
>    use SMLnj or MLton for their work. To date there is an issue of
>    source-based bootstrapping of _all_ of the major ML compilers. We do
>    have PolyML in our repositories, but even this uses space-inefficient
>    text file blobs for compiling and is not a fully C-based source
>    bootstrap. Basically, all of the ML compilers rely on some distinct
>    pre-compiled something-or-other to get to their pristine state. I
>    have explored the idea, along with Leo and Amin, about following in
>    the tradition of MES (and mrustc) and starting an analogous GNU project for
>    writing a reduced-size specification ML bootstrapping compiler. That
>    way we can end the loop of a source-based build of ML97 compilers
>    being basically impossible.
>    [See issues #38605 & #38606 on DEBBUGS. Also, see

It is a ambitious research project. Woow! Nice!! :-)

CakeML [1] claims to be a subset of Standard ML and to be
boostrappable. I do not know enough to have an relevant opinion.


What is the status of OCaml about boostrappability?

> -- Begin giving talks on the benefits of GNU Guix at conferences around
>    Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

Yes, let spread the world! :-)

And IMO a good start is to show in scientific communities why
boostrappability matters.

For example, the papers which were OK in [2] (2015), are they still OK
in 2019? I bet that a lot of big binary blobs have disappear since


All the best,

reply via email to

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