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
