From mboxrd@z Thu Jan 1 00:00:00 1970 From: Brett Gilio Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Mon, 16 Dec 2019 21:27:30 -0600 Message-ID: <874kxzzl5p.fsf@posteo.net> References: <87tv616q5s.fsf@posteo.net> <141B1FAE-6518-4E0C-8E69-C96BCB540545@lepiller.eu> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:38564) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ih3WI-00021t-RA for guix-devel@gnu.org; Mon, 16 Dec 2019 22:27:36 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ih3WH-0007ne-2h for guix-devel@gnu.org; Mon, 16 Dec 2019 22:27:34 -0500 Received: from mout02.posteo.de ([185.67.36.66]:57745) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ih3WG-0007l8-Ge for guix-devel@gnu.org; Mon, 16 Dec 2019 22:27:33 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id 92CBC2400FD for ; Tue, 17 Dec 2019 04:27:30 +0100 (CET) In-Reply-To: <141B1FAE-6518-4E0C-8E69-C96BCB540545@lepiller.eu> (Julien Lepiller's message of "Mon, 16 Dec 2019 09:47:55 +0100") 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: Julien Lepiller Cc: guix-devel@gnu.org, janekke@gnu.org, bandali@gnu.org Julien Lepiller writes: > OCaml stuff can easily be imported with guix import opam. I know coq > packages use a separate opam repository, so it would be nice if the > importer could take an optional parameter to indicate a custom opam > repository url. I'm not sure the coq repo is converted to opam 2 yet > though. To my knowledge the Coq repo is not compliant with OPAM 2 quite yet. Maybe this has changed since I last checked, but I would be more than happy to ask upstream if this is still the case. I think working on an importer for those modified OPAM->Coq packages would be a fantastic start to that problem. > I can see the benefits of formal methods and benefits of guix, but > what does guix provide or could provide to formal method people > specifically? Is it "only" the nice guarantees it gives to any > programer, or is there something else? Maybe the question is why does > it matter more to fm people than to other programmers? I think it is a combination of what every other programmer is offered, and the possibilities offered by what bootstrapping has to offer for creating a machine from "nothing". There is still a lot of unknowns here, but I speculate that there is definitely more to be found as the concept progresses. I think your question is valid, and should likely be a central thesis to the working group; "What does Guix offer to the formal methods community that it could specifically benefit from?" > I think we're still a small community, so we can continue talking > about it on the main channel. 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. We also always hear about > bootstrapping or the hpc effort on the main channel. Let's talk about > fm :). You can count me in. Agreed, lets not separate the community. Keep the communication integrated. Though, I wonder if maybe I could draft an article for the Guix website blog; or maybe we could organize our goals somewhere? I am not quite sure what the best option here is. For example, one of the goals is a possible bootstrapping compiler for ML that I mentioned before, that would be dedicated to the GNU project in a similar fashion to Jan's GNU Mes (which, thank you Jan for the supportive messages). Combine this on maybe working out a bootstrap for OCaml, creating an importer for Coq, working on some more programming research-related questions in the context of Guix and suddenly we have ourselves a trifecta of big questions that need to be articulated _somewhere_ so we can retain some scope. Maybe Guix needs a wiki similar to the wishlist, but dedicated to working groups? I really have no idea. Just something, somewhere to centralize our goals. Regardless, thank you for the supportive voice Julien. I am glad to have your support. -- Brett M. Gilio GNU Guix, Contributor