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