From mboxrd@z Thu Jan 1 00:00:00 1970 From: Julien Lepiller Subject: Re: [Proposal] The Formal Methods in GNU Guix Working Group Date: Mon, 16 Dec 2019 21:10:40 +0100 Message-ID: <1D33E23C-E6D6-4410-AAEF-75FE64A1E785@lepiller.eu> References: <87tv616q5s.fsf@posteo.net> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:55829) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1igwhj-0008FY-Ez for guix-devel@gnu.org; Mon, 16 Dec 2019 15:10:56 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1igwhh-0003ef-SC for guix-devel@gnu.org; Mon, 16 Dec 2019 15:10:55 -0500 Received: from lepiller.eu ([2a00:5884:8208::1]:53418) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1igwhh-0003QH-Cm for guix-devel@gnu.org; Mon, 16 Dec 2019 15:10:53 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 5db6e661 for ; Mon, 16 Dec 2019 20:10:49 +0000 (UTC) Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id c6df2036 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 16 Dec 2019 20:10:48 +0000 (UTC) In-Reply-To: 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: guix-devel@gnu.org Le 16 d=C3=A9cembre 2019 20:46:28 GMT+01:00, zimoun a =C3=A9crit : >Hi, > >I am not a Programming Language Theory guy so I speak as a pure noob=2E >:-) >Well, I am working in University Paris 7 Diderot doing some scientific >computing=2E > > >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=2E > >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)=2E >And yes, the reproducibility over the time means bootstrappability=2E >But it is each scientific community that must take care of its >outputs=2E > >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=2E > >And what I see as a blocking wider adoption by the Researcher around >me is: Mac=2E 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=2E > >I know the article by Ludo and Ricardo=2E :-) And I strongly agree=2E >From my point of view, the only way to attract more researchers is to >have an half-baked Guix working on Mac, IMHO=2E > > >> -- A lot of proof assistants are based on dialects of ML=2E Most of >these >> use SMLnj or MLton for their work=2E To date there is an issue of >> source-based bootstrapping of _all_ of the major ML compilers=2E 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=2E Basically, all of the ML compilers rely on some >distinct >> pre-compiled something-or-other to get to their pristine state=2E 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=2E >That >> way we can end the loop of a source-based build of ML97 compilers >> being basically impossible=2E >> [See issues #38605 & #38606 on DEBBUGS=2E Also, see >> https://github=2Ecom/MLton/mlton/issues/350=2E] > >It is a ambitious research project=2E Woow! Nice!! :-) > >CakeML [1] claims to be a subset of Standard ML and to be >boostrappable=2E I do not know enough to have an relevant opinion=2E > >[1] https://cakeml=2Eorg/ > >What is the status of OCaml about boostrappability? I'm afraid OCaml is not bootstrappable=2E It uses a bytecode version of it= self (using a bootstrapped bytecode interpreter written in C) to build itse= lf=2E Fortunately this situation is being worked on by a phd student of Xav= ier Leroy (and nixOS user) :)=2E The plan is to write a compiler in C or Scheme (it currently exists, but i= s written in OCaml) for "miniML" a small subset of the OCaml language=2E Th= en, there is already an interpreter in miniML able to interpret the OCaml c= ompiler compiling itself=2E Once the miniML compiler is bootstrapped, we wi= ll have a path from C to OCaml :) > > >> -- Begin giving talks on the benefits of GNU Guix at conferences >around >> Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc=2E > >Yes, let spread the world! :-) > >And IMO a good start is to show in scientific communities why >boostrappability matters=2E > >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=2E > >[2] http://repeatability=2Ecs=2Earizona=2Eedu/ > > > >All the best, >simon