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

[zimoun <zimon.toutoune@gmail.com>]

Hi,

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
computing.


On Mon, 16 Dec 2019 at 02:00, Brett Gilio <brettg@posteo.net> 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
outputs.

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
>    https://github.com/MLton/mlton/issues/350.]

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.

[1] https://cakeml.org/

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
then.

[2] http://repeatability.cs.arizona.edu/



All the best,
simon