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

[Brett Gilio]

zimoun <address@hidden> writes:

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

We are all noobs of formal methods next to Vladimir Voevodsky, and
Grothendiek. ;)

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

Undoubtedly the formal methods community, just as with all other
communities of scientific research stands to benefit from the
time-machine! No question about that. I would be intrigued to see in
what ways we can push that paradigm to its limits. Formal methods is
notorious for finding novel ways to bring change to our systems of
abstraction, and challenge our notions of things like "safety". So maybe
the time-machine could still stand to benefit from improvement, and maybe the 
formal
methods community by using it will find out ways to do that. Purely
speculation, here.

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

I am quite familiar with CakeML, and I draw a lot of inspiration with
the things they are managing to do as a subset implementation of ML. I
think it would be interesting to see where a bootstrapping compiler
could go if it were fledged out into a full implementation for the GNU
project, filling a dual-role. Again, just proposing some ideas. :)

> What is the status of OCaml about boostrappability?

Julien answered this already, but there is a gap here.

> 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

Simon, I am glad to have your support here! Please engage with us more
as more details come. You may be a "noob" (self-reported), but it is
noobs who provide us the most valuable information often times.

-- 
Brett M. Gilio <address@hidden>
GNU Guix, Contributor <https://guix.gnu.org/>