From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:43278) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ignDT-0001gg-JO for guix-patches@gnu.org; Mon, 16 Dec 2019 05:03:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ignDS-0003za-B3 for guix-patches@gnu.org; Mon, 16 Dec 2019 05:03:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:60185) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ignDS-0003zI-7j for guix-patches@gnu.org; Mon, 16 Dec 2019 05:03:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ignDS-0005UF-1y for guix-patches@gnu.org; Mon, 16 Dec 2019 05:03:02 -0500 Subject: [bug#38605] [WIP MLton 0/1] Add MLton Resent-Message-ID: From: Ludovic =?UTF-8?Q?Court=C3=A8s?= References: <877e2z7e3x.fsf@posteo.net> <87v9qix001.fsf@gnu.org> <87y2vd43uo.fsf@posteo.net> Date: Mon, 16 Dec 2019 11:02:35 +0100 In-Reply-To: <87y2vd43uo.fsf@posteo.net> (Brett Gilio's message of "Sun, 15 Dec 2019 16:32:31 -0600") Message-ID: <87tv60k2pw.fsf@gnu.org> 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: Brett Gilio Cc: 38605@debbugs.gnu.org Hi Brett, Brett Gilio skribis: > It's a little off of the subject at hand, but to my knowledge (as > provided by this issue: https://github.com/MLton/mlton/issues/350) I am > going to cherry pick a few things of note. Thanks for discussing it with upstream! Your reply summarizes current =E2=80=9Cbest practices=E2=80=9D pretty well: for Rust, for Guile (which co= ntains an interpreter in C), for Common Lisp (GNU=C2=A0clisp is written in C), for C (MesCC), etc. > I wonder if the best long-term solution for melding Guix and the ML > language community is to try and write an ML compiler in a language like > C or Scheme based on a reduced-sized specification of the language. I vaguely recall reading about an SML implementation in Scheme. All I could find is a mention of it in . > The reason I say all this is because I would really love to see the > philosophies of ML/Formal Methods/Proof and the deterministic/functional > philosophy of Guix work together. They seem naturally synergistic, but > there seems be a difference in history here that is making this quite > antagonistic. > > I'd really like to spark some insight and discussion here because it > would be amazing if the formal methods community (like Coq, seL4, > HOL/Isabelle, etc.) could really begin to benefit from the Guix model. I agree that the two should be synergistic. Eventually, all this comes down to how to design a programming language or its implementation in a way that allows is to be built incrementally from =E2=80=9Cnothing=E2=80=9D= , or from a different language (something janneke and I discussed at the R-B summit). This sounds very much like programming language research question. Thanks, Ludo=E2=80=99.