Ludovic Courtès <l...@gnu.org> writes: > For the record, I don’t work with the formal methods people at Inria, > but we chat occasionally, and I’d be happy to draw their attention 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’s sounds very ambitious, though it’s not like people here haven’t > 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’s an alternative tradition of theorem provers in Lisp > with ACL2, “The Little Prover”, 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 (‘guix > environment’, channels like Julien’s Coq channel), and so on. > > These things take time and we don’t necessarily have an idea what the > outcome should be, but it’s 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! -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] <bre...@gnu.org> <bre...@posteo.net>