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: Sat, 21 Dec 2019 17:59:19 -0600 Message-ID: <8736ddcjs8.fsf@gnu.org> References: <87tv616q5s.fsf@posteo.net> <877e2qqilt.fsf@gnu.org> Mime-Version: 1.0 Content-Type: text/plain Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:45841) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iioeb-0003Zw-Vv for guix-devel@gnu.org; Sat, 21 Dec 2019 18:59:27 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:36465) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1iioeb-00057k-Qv for guix-devel@gnu.org; Sat, 21 Dec 2019 18:59:25 -0500 In-Reply-To: <877e2qqilt.fsf@gnu.org> (Amin Bandali's message of "Sat, 21 Dec 2019 01:48:46 -0500") 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 Cc: bandali@gnu.org =2D----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Amin Bandali writes: > Hello Guix! > > Thank you Brett for taking initiative and putting this awesome proposal > together on all our behalves, and to everyone else for chiming in and > expressing your interest and support! > > To share some of my (scattered) thoughts on this, as a researcher I > think reproducible and verifiable research is a crucially important > topic, yet traditionally and often a neglected one. Throughout my > graduate studies, too many times I stumbled on papers with interesting > claims that I sadly could not reproduce or easily verify for myself. > And I think this is especially ironic and painful for those of us doing > research in formal methods, computing science, and software engineering; > and is where projects like GNU Guix with their awesome efforts in > reproducibility could act as role models and show what's possible. > > For instance, for better or worse many of the tools I have worked with > over the last few years are primarily implemented in Java, often in form > Eclipse plugins. Suffice to say that release management, bundling, and > distribution practices of most of these tools leave a lot to be desired. > As part of the Formal Methods in GNU Guix Working Group, I'd love for us > to try and get in touch with the developers of these tools and offer to > work with them to challenge and improve the status quo, resulting > ultimately in more readily and easily accessible tools, greatly useful > for verifying and reproducing existing literature. > > As Brett and I alluded to, there's a large variety of tasks in all > shapes and sizes that could use your help, from more "researchy" work > like writing a bootstrapping SML '97 compiler, or exploring synthesis > and verification for GNU Guile and GNU Guix, to less researchy ones like > packaging (even more) formal methods-related software and helping their > developers improve their release and package qualities. > > We would love to hear more from you about this in trying to gradually > put together actionable plans. If you'd like to chat with us, please > come say hi to us in the #guix IRC channel on freenode. My nick there > is bandali, and Brett is brettgilio. > > Best, > amin > Hello, everybody! Thank you, Amin for your substantial contribution in this last email. I am 100% in agreement with your assessment, and there is definitely a plethora of work to be done here! To kick-start the project I am wanting to make some suggestions, mostly pertaining to the organization and up-keep of the working group. 1. Just as the bootstrappability and guix-hpc projects have their own websites documenting their efforts, I think it would be nice to have https://fm.guix.gnu.org/ which would host a Haunt-generated website. This website would be hosted in the Savannah project structure for GNU Guix. This would document who is active in the coordination and oversight of this working group, and would express a clear and mutual relationship with the GNU Guix / Guix System project. 2. Perhaps we should adopt a particular tag for the Guix Debbugs tracker, so as to be able to clearly delineate that this particular patch or bug is in relation with the formal methods working group. Maybe something like [FM]. 3. It was suggested that maybe a #guix-fm IRC channel might be useful, but we have had a mixed bag of opinions on this. I personally think that keeping everything together is the better solution, but I'd still like to hear acceptance or criticism of this idea. 4. A lot of documenting working group milestones (Working on a Coq sub-importer for OPAM, writing a bootstrapping compiler for SML97, doing regular packaging duties for formal methods projects, communicating upstream about distribution package quality, and perhaps even trying to do formal methods work via synthesis in GNU Guile / GNU Guix would be likely best expressed on the mailing list, and the https://fm.guix.gnu.org/ website, but this likely rests in the hands of the GNU Guix maintainers, of which I am not. 5. Additionally, maybe making an introductory post on the https://guix.gnu.org/ blog about the preliminary goals of the working group, after having our own subdomain established, would be a good way to attract some attention to the project by distributing links to it on HackerNews, Reddit, and Formal Methods/Functional Programming-related mailing lists. Anyways, I am going to CC Ludo' in this message to see what he might have to say about these proposals. Thanks for everybody who has chimed in! =2D --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] =2D----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE38DH957mDKeuVV4ZZyJDxKA/Du4FAl3+sdcACgkQZyJDxKA/ Du7YyhAAqEZqbOO1W37xKvd8EztAp/dYJ1Q9Bt/mw9eH0Aj95lxkFQkl9Iq+Bvqa DGPiVeyR7nOn/AtKdZMwrgz9xZXE43pQ1C8IV8+Jbssv9l3G2UQdzwIiP4YyFKum Lj7kkNEKC5GZ9CpgMcSHGevmW+YpTcTIVOZWFve/4eera27Ds9RMgME8q8FaKKLt CoYwi0JeHqUmlP+ZrYJ2KSPVyffxFZjW5W1SnrKoLtzp+w70j/E1m0kSr1SpPuZ2 sDwGK/gM3pQ8wHMxLwbP9MFU3S2lsqryr9Uiefca43He94KhrHOpq266nHH96FsF GfgflhYZfCuhm6gL7iZg/3valjAFcF0JJS59CymQ32DI9zgTnexeGjd9NXjl9kf7 X6J5/CuWrra7IDJ8f5/iqnF5XjS132R6a5jIJz5BwPDag8mqDKA2xKtb16FkND/I ZCcnI+EA8pXbh2awmNKoG0c6penPY5+falcCNJ/T2bn3KsXsk4JymwePYa38jYUr GCauYGt6W3DfauAHJ+maNjxvtsWIGP5+gIbG/JViClSndT6zHOBinHGdFobz5AjN fEdCx4kyoWo2rrmTrnWBuaDtNNPnuW0y8zx9qjQ9k9LXFAp1nyRJ46x1LVAhl+3U uvHhAWiVNLuqreLEJPitZE3lebwt9r2m7/VpKQH7UL8CVA3ws/o=3D =3DY0Ml =2D----END PGP SIGNATURE-----