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/
