Re: [Proposal] The Formal Methods in GNU Guix Working Group

[Brett Gilio]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Amin Bandali <address@hidden> 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!

- -- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<address@hidden> <address@hidden>
-----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=
=Y0Ml
-----END PGP SIGNATURE-----