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

[Julien Lepiller <julien@lepiller.eu>]

Le 16 décembre 2019 01:59:59 GMT+01:00, Brett Gilio <brettg@posteo.net> a écrit :
>Hello Guix!
>
> ...
>
>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.]
>
>-- 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!

OCaml stuff can easily be imported with guix import opam. I know coq packages use a separate opam repository, so it would be nice if the importer could take an optional parameter to indicate a custom opam repository url. I'm not sure the coq repo is converted to opam 2 yet though.

>-- 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?
>
>-- Begin giving talks on the benefits of GNU Guix at conferences around
>   Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

I can see the benefits of formal methods and benefits of guix, but what does guix provide or could provide to formal method people specifically? Is it "only" the nice guarantees it gives to any programer, or is there something else? Maybe the question is why does it matter more to fm people than to other programmers?

>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 think we're still a small community, so we can continue talking about it on the main channel. We're trying to avoid dividing information, that's why we allow any language on tge channel, instead of having separate chans for each language. We also always hear about bootstrapping or the hpc effort on the main channel. Let's talk about fm :). You can count me in.

>I hope to hear from the community.
>
>Thanks,