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: Fri, 27 Dec 2019 21:06:20 -0600 Message-ID: <871rspqhcj.fsf@gnu.org> References: <87tv616q5s.fsf@posteo.net> <87sgl5cojg.fsf@gnu.org> 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]:43935) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1il2Qq-0006ED-0Z for guix-devel@gnu.org; Fri, 27 Dec 2019 22:06:25 -0500 In-Reply-To: <87sgl5cojg.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Sat, 28 Dec 2019 00:54:43 +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: Ludovic =?utf-8?Q?Court=C3=A8s?= Cc: guix-devel@gnu.org, bandali@gnu.org, leo.prikler@student.tugraz.at Ludovic Court=C3=A8s writes: > For the record, I don=E2=80=99t work with the formal methods people at In= ria, > but we chat occasionally, and I=E2=80=99d be happy to draw their attentio= n to > this effort. :-) I thought not, but I think this smells of potential for collaboration maybe amongst a few there. I know some INRIA people from the Caml and Coq community, so I think if they see a notification both internally and externally of what is happening with this proposal (after we establish it a bit more) it has the potential to get some attention. > That=E2=80=99s sounds very ambitious, though it=E2=80=99s not like people= here haven=E2=80=99t > been ambitious so far. ;-) It is absolutely an ambitious task, and is definitely a daunting one to try and make happen. I do have some experience with compiler construction, but nothing quite to this extent. Amin and I have been trying to establish connections with other people who might share this goal, and from what we've received it is _this_ particular task of making a bootstrapping compiler for ML that seems to be the most attention-getting. There is definitely a need here, we realized. So, if we are able to garner enough people to help make this task more manageable then I say it is in the realm of possibility and will prove useful for Guix. > Note that there=E2=80=99s an alternative tradition of theorem provers in = Lisp > with ACL2, =E2=80=9CThe Little Prover=E2=80=9D, etc. I am familiar :). The Little Prover and the Little Typer are foundational to my interest here. I have not considered ways to include them, so food for thought! > 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= on. > > These things take time and we don=E2=80=99t necessarily have an idea what= the > outcome should be, but it=E2=80=99s definitely worthwhile. Agreed! 100%. We have a lot of lateral connection making to do, and I will help foster that any way I can. By the sound of it, Amin has already been working with some of the Lean prover people on Zulip to see what is possible for attracting some attention there. I will do my part on this as well, and once we get an organizational page made for the working group at whatever address it exists at, I think we will be able to get some cross-pollination like we need. I definitely want to do this the "right way". Thank you Ludo for your help! --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]