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

[Jack Hill <jackhill@jackhill.us>]

[-- Attachment #1: Type: text/plain, Size: 4604 bytes --]

Greetings,

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
>   https://github.com/MLton/mlton/issues/350.]

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

[0] https://elephly.net/posts/2017-01-09-bootstrapping-haskell-part-1.html

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

Thanks for proposing the idea!

All the best,
Jack