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

[Brett Gilio <brettg@gnu.org>]

Ludovic Courtès <ludo@gnu.org> writes:

> For the record, I don’t work with the formal methods people at Inria,
> but we chat occasionally, and I’d be happy to draw their attention to
> this effort.  :-)

I thought not, but I think this smells of potential for collaboration
maybe amongst a few there. I know some INRIA people from the Caml and
Coq community, so I think if they see a notification both internally and
externally of what is happening with this proposal (after we establish
it a bit more) it has the potential to get some attention.

> That’s sounds very ambitious, though it’s not like people here haven’t
> been ambitious so far.  ;-)

It is absolutely an ambitious task, and is definitely a daunting one to
try and make happen. I do have some experience with compiler
construction, but nothing quite to this extent. Amin and I have been
trying to establish connections with other people who might share this
goal, and from what we've received it is _this_ particular task of
making a bootstrapping compiler for ML that seems to be the most
attention-getting. There is definitely a need here, we realized. So, if
we are able to garner enough people to help make this task more
manageable then I say it is in the realm of possibility and will prove
useful for Guix.

> Note that there’s an alternative tradition of theorem provers in Lisp
> with ACL2, “The Little Prover”, etc.

I am familiar :). The Little Prover and the Little Typer are
foundational to my interest here. I have not considered ways to include
them, so food for thought!


> I agree with Julien that a separate IRC channel is unneeded at this
> stage; as for the structure, I would start with a web page explaining
> your areas of interests, similar to the Guix-HPC thing.
>
> To me, an important goal is to create ties with formal methods people,
> and to increase the bandwidth between us.  That can beget new ideas and
> perspectives.
>
> Then there are specific areas where we should be discussing: compiler
> bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make
> their compilers bootstrappable?), package management (how to turn OPAM,
> etc. into functional package managers, or how to get language X to use
> Guix instead of rolling its own?), development facilities (‘guix
> environment’, channels like Julien’s Coq channel), and so on.
>
> These things take time and we don’t necessarily have an idea what the
> outcome should be, but it’s definitely worthwhile.

Agreed! 100%. We have a lot of lateral connection making to do, and I
will help foster that any way I can. By the sound of it, Amin has
already been working with some of the Lean prover people on Zulip to see
what is possible for attracting some attention there. I will do my part
on this as well, and once we get an organizational page made for the
working group at whatever address it exists at, I think we will be able
to get some cross-pollination like we need. I definitely want to do this
the "right way".

Thank you Ludo for your help!

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>