[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Jack Hill
Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group
Date: Mon, 16 Dec 2019 18:04:40 -0500 (EST)
User-agent: Alpine 2.20 (DEB 67 2015-01-07)


On Sun, 15 Dec 2019, Brett Gilio wrote:

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.


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.

I'm not a formal methods researcher, but merely a hobbyist who is interested in programming languages and type system. That said, I find this proposal intriguing, and would like to follow along, and perhaps help as I am able. At the very least, I hope to learn some new things.

One of the things that attracted me to Guix is the ability to represent the pieces as objects in a programming language as opposed the the big mass of state that is a traditional system. I agree this property of Guix harmonizes with formal analysis.


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]

This is the sub-area I'm most interested in. In addition to ML, I'd also like to be able to bootstrap GHC. I know that Ricardo has done some work in that area [0].


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

I would love to have more tools like these in Guix, so that we can use Guix's repoducibility guarantees to have them as part of the historical record.

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

I hope to hear from the community.

Thanks for proposing the idea!

All the best,

reply via email to

[Prev in Thread] Current Thread [Next in Thread]