[Proposal] The Formal Methods in GNU Guix Working Group

[Brett Gilio]

Hello Guix!

This is going to be a rather lengthy email proposing a new working group
(if that is indeed the proper name for this) in the GNU Guix
project. Just as there are other "working groups" for GNOME packages,
bootstrapping Rust & JVM, and bootstrapping the entirely of the GNU
Corelibs (GNU Mes) in Guix, I am proposing a new working group based on
the synthesis of two fundamentally and mutually agreeable concepts.

This is a continuation of the discussion proposed by Amin Bandali, Leo
Prikler, and I from the #guix Freenode IRC. All three of us are either
students of formal methods in mathematics and computer science, users of
proof assistants, or interested in category theory and type theory. As
such as noticed and wondered what kind of community there is for formal
methods in GNU Guix, and by extension what kind of benefits GNU Guix has
to offer the formal methods community which is providing some of the
most rigorous research in computing methods to date.

First, some background. For those of you unfamiliar with formal methods
and software verification in computer science, it is by-and-large
applications of mathematical proof to the conceptions of how we design
our software. We design our software around proofs that have a certain
level of correctness thus we do not have to speculate about the behavior
of that software. To me that has a striking resemblence to the less
rigorous but all-the-more impressive goal of Guix to be functionally
deterministic. Many of the concepts of formal methods take from untyped
(and typed) lambda calculus and are then abstracted to have higher-order
guarantees in their construction.

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.

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!

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

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 hope to hear from the community.

Thanks,

-- 
Brett M. Gilio
Homepage -- https://scm.pw/
GNU Guix -- https://guix.gnu.org/