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

[Ludovic Courtès]

Hi!

Brett Gilio <address@hidden> skribis:

> Having Guix and the Formal Methods community aligned would mean a great
> deal of power for both camps! Just as we see with the Software Heritage
> project and Guix, for providing historical and state-consistent
> reproducible environments for software testing we and correspond to
> formal methods much of the same guarantees of deterministic
> computational states, modeling, and reasoning in software correctness.
>
> Amin, Leo, and I all likely agree that _some_ relationship here is good
> to be opened and explored! I know that there are some of us who come
> from institutions that have historical relationships to the proof
> assistant community, Caml, HOL (looking at you Ludo', though IIRC you
> are in a different working group at INRIA),
> so this could be more of a chance to see bigger institutions begin to
> adopt Guix for their research work.

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

> What follows is proposals for some of the work to be done by this
> working group:
>
> -- 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.]

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

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

> -- Begin adding more projects that are important works in the formal
>    methods community. We have Coq, Idris, and Agda, but there is a lot of work
>    to be done on keeping these projects not only up-to-date but also
>    adding subprojects that use these toolchains. For example: C Minor,
>    Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
>    RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
>    various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
>    Haskell, extensions to Z3, and tons more!

+1

> -- Possibly begin formally verifying some of the behavior and
>    implementations of GNU Guix and GNU Guile. This is kind of an add-on
>    idea, but it struck our interest so why leave it out?

Put this way, it seems very broad.  One thing I’d like to have is (1)
Racket-style contracts, in particular for our record types, and (2)
Turnstile-style static type checking, again primarily for record types.

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

+1!

> All of this seems really nice and impressive, but what is it without
> getting some feedback from the community? I'd _really_ love to hear your
> thoughts, experiences, and more on this working group idea and other
> working groups to avoid pitfalls. Maybe we should have a secondary
> #guix-fm channel on IRC? There is definitely a lot of work to be done
> here, and we will need some form of organizational structure to keep the
> work consistent and neatly integrated with the goals and purposes of GNU
> Guix.

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.

Thanks,
Ludo’.