From mboxrd@z Thu Jan 1 00:00:00 1970 From: zimoun Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Mon, 16 Dec 2019 20:46:28 +0100 Message-ID: References: <87tv616q5s.fsf@posteo.net> Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:47299) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igwKL-0000ZB-Ee for guix-devel@gnu.org; Mon, 16 Dec 2019 14:46:47 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igwKJ-0003lC-7w for guix-devel@gnu.org; Mon, 16 Dec 2019 14:46:45 -0500 In-Reply-To: <87tv616q5s.fsf@posteo.net> 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: Brett Gilio Cc: Guix Devel , leo.prikler@student.tugraz.at, Amin Bandali 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. On Mon, 16 Dec 2019 at 02:00, Brett Gilio wrote: > 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. And what I see as a blocking wider adoption by the Researcher around me is: Mac. A lot of them just use Mac, I mean they develop daily on MacOS and then once it is ready run on linux HPC clusters. I know the article by Ludo and Ricardo. :-) And I strongly agree. >From my point of view, the only way to attract more researchers is to have an half-baked Guix working on Mac, IMHO. > -- 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/ What is the status of OCaml about boostrappability? > -- Begin giving talks on the benefits of GNU Guix at conferences around > Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc. 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