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:48:54 -0600 Message-ID: <87mubry5ll.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]:45662) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ih3r0-0006Af-RN for guix-devel@gnu.org; Mon, 16 Dec 2019 22:49:00 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ih3qz-00051F-Dq for guix-devel@gnu.org; Mon, 16 Dec 2019 22:48:58 -0500 Received: from mout01.posteo.de ([185.67.36.65]:42668) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ih3qy-0004zp-Rd for guix-devel@gnu.org; Mon, 16 Dec 2019 22:48:57 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id 6377E160060 for ; Tue, 17 Dec 2019 04:48:55 +0100 (CET) In-Reply-To: (Jack Hill's message of "Mon, 16 Dec 2019 18:04:40 -0500 (EST)") 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: Jack Hill Cc: guix-devel@gnu.org, leo.prikler@student.tugraz.at, bandali@gnu.org Jack Hill writes: > I'm not a formal methods researcher, but merely a hobbyist who is > interested in programming languages and type system. That said, I find > this proposal intriguing, and would like to follow along, and perhaps > help as I am able. At the very least, I hope to learn some new things. I am glad you say this. We all have a lot to learn from each other here. > One of the things that attracted me to Guix is the ability to > represent the pieces as objects in a programming language as opposed > the the big mass of state that is a traditional system. I agree this > property of Guix harmonizes with formal analysis. Absolutely! This is the kind of thesis I was proposing, and something that I wonder what Julien will think of as far as benefits particular and specific to the formal methods community. >> What follows is proposals for some of the work to be done by this >> working group: >> >> -- 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.] > > This is the sub-area I'm most interested in. In addition to ML, I'd > also like to be able to bootstrap GHC. I know that Ricardo has done > some work in that area [0]. > > [0] > https://elephly.net/posts/2017-01-09-bootstrapping-haskell-part-1.html So far this idea has garnered the most attention. Amin Bandali and I are both wanting to see this be taken to the next level, with maybe the support of Janneke and other people working with minimal compilers / formal methods in their day-to-day work. See some of my previous emails to others about why I think this is important work. Basically, as I mentioned to Ludo' the situation of bootstrapping ML from source is occluded after 1993. We should reasonably be able to remedy this in order to facilitate ML-based proof assistant development and use on Guix. Especially things like the PRLs (NuPRL, RedPRL, JonPRL) which offer nice dependent type systems. But first the compiler tower needs to be there." Maybe we could borrow some inspiration from miniML (mentioned by Julien), CakeML (mentioned by Simon), or C Minor? I don't know. But I think this is an important task. > Thanks for proposing the idea! > > All the best, > Jack Thank you for voicing your support Jack! :) -- Brett M. Gilio GNU Guix, Contributor