From mboxrd@z Thu Jan 1 00:00:00 1970 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Sat, 28 Dec 2019 00:54:43 +0100 Message-ID: <87sgl5cojg.fsf@gnu.org> References: <87tv616q5s.fsf@posteo.net> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:45189) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ikzRR-0005v9-W9 for guix-devel@gnu.org; Fri, 27 Dec 2019 18:54:51 -0500 In-Reply-To: <87tv616q5s.fsf@posteo.net> (Brett Gilio's message of "Sun, 15 Dec 2019 18:59:59 -0600") List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: Brett Gilio Cc: guix-devel@gnu.org, leo.prikler@student.tugraz.at, bandali@gnu.org Hi! Brett Gilio skribis: > 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. For the record, I don=E2=80=99t work with the formal methods people at Inri= a, but we chat occasionally, and I=E2=80=99d be happy to draw their attention = to this effort. :-) > 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 projec= t 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.] That=E2=80=99s sounds very ambitious, though it=E2=80=99s not like people h= ere haven=E2=80=99t been ambitious so far. ;-) Note that there=E2=80=99s an alternative tradition of theorem provers in Li= sp with ACL2, =E2=80=9CThe Little Prover=E2=80=9D, etc. > -- 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! +1 > -- 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? Put this way, it seems very broad. One thing I=E2=80=99d like to have is (= 1) Racket-style contracts, in particular for our record types, and (2) Turnstile-style static type checking, again primarily for record types. > -- Begin giving talks on the benefits of GNU Guix at conferences around > Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc. +1! > 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 agree with Julien that a separate IRC channel is unneeded at this stage; as for the structure, I would start with a web page explaining your areas of interests, similar to the Guix-HPC thing. To me, an important goal is to create ties with formal methods people, and to increase the bandwidth between us. That can beget new ideas and perspectives. Then there are specific areas where we should be discussing: compiler bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make their compilers bootstrappable?), package management (how to turn OPAM, etc. into functional package managers, or how to get language X to use Guix instead of rolling its own?), development facilities (=E2=80=98guix environment=E2=80=99, channels like Julien=E2=80=99s Coq channel), and so o= n. These things take time and we don=E2=80=99t necessarily have an idea what t= he outcome should be, but it=E2=80=99s definitely worthwhile. Thanks, Ludo=E2=80=99.