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

[Julien Lepiller <julien@lepiller.eu>]

Le 16 décembre 2019 20:46:28 GMT+01:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>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?

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 :)

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