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: Mon, 16 Dec 2019 21:38:08 -0600 Message-ID: <87v9qfy63j.fsf@posteo.net> References: <87tv616q5s.fsf@posteo.net> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:41785) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ih3gg-0003gD-RR for guix-devel@gnu.org; Mon, 16 Dec 2019 22:38:20 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ih3gf-0002pL-BU for guix-devel@gnu.org; Mon, 16 Dec 2019 22:38:18 -0500 Received: from mout02.posteo.de ([185.67.36.66]:58305) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ih3ge-0002jd-QH for guix-devel@gnu.org; Mon, 16 Dec 2019 22:38:17 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id 43F382400FD for ; Tue, 17 Dec 2019 04:38:14 +0100 (CET) In-Reply-To: (zimoun's message of "Mon, 16 Dec 2019 20:46:28 +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: zimoun Cc: Guix Devel , leo.prikler@student.tugraz.at, Amin Bandali zimoun writes: > Hi, > > I am not a Programming Language Theory guy so I speak as a pure noob. :-) > Well, I am working in University Paris 7 Diderot doing some scientific > computing. We are all noobs of formal methods next to Vladimir Voevodsky, and Grothendiek. ;) >> so this could be more of a chance to see bigger institutions begin to >> adopt Guix for their research work. > > IMHO, today the "win" is not about bootstrapping because it is > strongly language dependent but this "win" offered by Guix is about > the time-traveling reproducibility tools: today the key point in > scientific research (IMHO). > And yes, the reproducibility over the time means bootstrappability. > But it is each scientific community that must take care of its > outputs. > > The wider adoption could come from features as "time-machine", > available packages (channels for the not GNU compliant), easy to > distribute, to reproduce, be able to search in all the packages over > all the Guix history, etc. Undoubtedly the formal methods community, just as with all other communities of scientific research stands to benefit from the time-machine! No question about that. I would be intrigued to see in what ways we can push that paradigm to its limits. Formal methods is notorious for finding novel ways to bring change to our systems of abstraction, and challenge our notions of things like "safety". So maybe the time-machine could still stand to benefit from improvement, and maybe the formal methods community by using it will find out ways to do that. Purely speculation, here. >> -- A lot of proof assistants are based on dialects of ML. Most of these >> use SMLnj or MLton for their work. To date there is an issue of >> source-based bootstrapping of _all_ of the major ML compilers. We do >> have PolyML in our repositories, but even this uses space-inefficient >> text file blobs for compiling and is not a fully C-based source >> bootstrap. Basically, all of the ML compilers rely on some distinct >> pre-compiled something-or-other to get to their pristine state. I >> have explored the idea, along with Leo and Amin, about following in >> the tradition of MES (and mrustc) and starting an analogous GNU project for >> writing a reduced-size specification ML bootstrapping compiler. That >> way we can end the loop of a source-based build of ML97 compilers >> being basically impossible. >> [See issues #38605 & #38606 on DEBBUGS. Also, see >> https://github.com/MLton/mlton/issues/350.] > > It is a ambitious research project. Woow! Nice!! :-) > > CakeML [1] claims to be a subset of Standard ML and to be > boostrappable. I do not know enough to have an relevant opinion. > > [1] https://cakeml.org/ I am quite familiar with CakeML, and I draw a lot of inspiration with the things they are managing to do as a subset implementation of ML. I think it would be interesting to see where a bootstrapping compiler could go if it were fledged out into a full implementation for the GNU project, filling a dual-role. Again, just proposing some ideas. :) > What is the status of OCaml about boostrappability? Julien answered this already, but there is a gap here. > Yes, let spread the world! :-) > > And IMO a good start is to show in scientific communities why > boostrappability matters. > > For example, the papers which were OK in [2] (2015), are they still OK > in 2019? I bet that a lot of big binary blobs have disappear since > then. > > [2] http://repeatability.cs.arizona.edu/ > > > > All the best, > simon Simon, I am glad to have your support here! Please engage with us more as more details come. You may be a "noob" (self-reported), but it is noobs who provide us the most valuable information often times. -- Brett M. Gilio GNU Guix, Contributor