From mboxrd@z Thu Jan 1 00:00:00 1970 From: Julien Lepiller Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Mon, 16 Dec 2019 09:47:55 +0100 Message-ID: <141B1FAE-6518-4E0C-8E69-C96BCB540545@lepiller.eu> 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]:45202) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igm36-0007Vb-6M for guix-devel@gnu.org; Mon, 16 Dec 2019 03:48:17 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igm34-00069Q-R8 for guix-devel@gnu.org; Mon, 16 Dec 2019 03:48:16 -0500 Received: from lepiller.eu ([2a00:5884:8208::1]:52856) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1igm34-00068f-8B for guix-devel@gnu.org; Mon, 16 Dec 2019 03:48:14 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 72f0efd9 for ; Mon, 16 Dec 2019 08:48:09 +0000 (UTC) Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 17999d6c (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 16 Dec 2019 08:48:08 +0000 (UTC) In-Reply-To: <87tv616q5s.fsf@posteo.net> 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: guix-devel@gnu.org Le 16 d=C3=A9cembre 2019 01:59:59 GMT+01:00, Brett Gilio a =C3=A9crit : >Hello Guix! > > =2E=2E=2E > >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=2E Most of these > use SMLnj or MLton for their work=2E To date there is an issue of > source-based bootstrapping of _all_ of the major ML compilers=2E 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=2E Basically, all of the ML compilers rely on some distinct > pre-compiled something-or-other to get to their pristine state=2E 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=2E That > way we can end the loop of a source-based build of ML97 compilers > being basically impossible=2E > [See issues #38605 & #38606 on DEBBUGS=2E Also, see > https://github=2Ecom/MLton/mlton/issues/350=2E] > >-- Begin adding more projects that are important works in the formal >methods community=2E 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=2E 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! OCaml stuff can easily be imported with guix import opam=2E I know coq pac= kages use a separate opam repository, so it would be nice if the importer c= ould take an optional parameter to indicate a custom opam repository url=2E= I'm not sure the coq repo is converted to opam 2 yet though=2E >-- Possibly begin formally verifying some of the behavior and > implementations of GNU Guix and GNU Guile=2E 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=2E I can see the benefits of formal methods and benefits of guix, but what do= es guix provide or could provide to formal method people specifically? Is i= t "only" the nice guarantees it gives to any programer, or is there somethi= ng else? Maybe the question is why does it matter more to fm people than to= other programmers? >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=2E 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=2E I think we're still a small community, so we can continue talking about it= on the main channel=2E We're trying to avoid dividing information, that's = why we allow any language on tge channel, instead of having separate chans = for each language=2E We also always hear about bootstrapping or the hpc eff= ort on the main channel=2E Let's talk about fm :)=2E You can count me in=2E >I hope to hear from the community=2E > >Thanks,