From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:47992) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ih2Uv-0002XE-5D for guix-patches@gnu.org; Mon, 16 Dec 2019 21:22:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ih2Us-0003eQ-1f for guix-patches@gnu.org; Mon, 16 Dec 2019 21:22:05 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:34602) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ih2Ur-0003eG-UW for guix-patches@gnu.org; Mon, 16 Dec 2019 21:22:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ih2Ur-0006Th-Pq for guix-patches@gnu.org; Mon, 16 Dec 2019 21:22:01 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: From: Brett Gilio References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> <87tv60k2pw.fsf@gnu.org> <87k16wdkx0.fsf@gnu.org> Date: Mon, 16 Dec 2019 20:20:45 -0600 In-Reply-To: <87k16wdkx0.fsf@gnu.org> ("Ludovic \=\?utf-8\?Q\?Court\=C3\=A8s\=22'\?\= \=\?utf-8\?Q\?s\?\= message of "Mon, 16 Dec 2019 22:23:39 +0100") Message-ID: <878snbzo8y.fsf@posteo.net> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Ludovic =?UTF-8?Q?Court=C3=A8s?= Cc: 38605@debbugs.gnu.org, bandali@gnu.org, zimoun Ludovic Court=C3=A8s writes: > Hi Simon, > > zimoun skribis: > >> To my knowledge, the most advanced ML-family language able to >> bootstrap (and verified with prover etc.) is CakeML (subset of >> Standard ML). >> >> (And not packaged in Guix, AFAICT.) >> >> https://cakeml.org/ > > Right, thanks for the pointer! CakeML is truly impressive. It=E2=80=99s= also > nice to see how the tiny diagram to the right of the web page clearly > and succinctly describes its compiler/language tower. > > Ludo=E2=80=99. I may be misspeaking, but I think CakeML is formally verified in HOL which bootstraps against PolyML or SMLnj, and also requires MLton. So the issue of cyclic binary-derived bootstrapping remains an issue. This is where I think Amin Bandali (CC) and I's idea of writing a C-based boostrapping compiler and dedicating it to the GNU project would be really valuable. Ultimately I think we need a vehicle for ML to be fledged out in Guix so that we can have a consistent set of utilities for the formal methods community to work in with Guix (see my formal methods working group proposal email). Maybe at some later date we could even fledge out that bootstrapping compiler to be its own distinct implementation of ML, but i'll save that for a later date. Regardless, the issue of binaries-on-binaries in ML seems to be reaching back to 1993! It's about time we ended that. Stay tuned for more information on what I think we could do about that. --=20 Brett M. Gilio GNU Guix, Contributor