From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 8092D7EEFD for ; Fri, 19 Jun 2015 00:26:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.172 as permitted sender) identity=mailfrom; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f172.google.com) identity=helo; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C+AQApRINVm6zVVdFcFoMZNV8Ggxi8SoVsCgKBOAdMAQEBAQEBEgEBAQEBBgsLCSEuhCMBAQICEhEdARsdAQMMBgULDQICJgICIQEBEQEFARwGEyKHdwEDEg2kWT4xiz+Ba4J5iy0KGScNV4UOAQEBAQYBAQEBGAEFDoETiiSCTYIGMweCaIFDBZNwhFOFF4FhgXaPGQmFRBIjgQwJgjEcgVQ8MYJIAQEB X-IPAS-Result: A0C+AQApRINVm6zVVdFcFoMZNV8Ggxi8SoVsCgKBOAdMAQEBAQEBEgEBAQEBBgsLCSEuhCMBAQICEhEdARsdAQMMBgULDQICJgICIQEBEQEFARwGEyKHdwEDEg2kWT4xiz+Ba4J5iy0KGScNV4UOAQEBAQYBAQEBGAEFDoETiiSCTYIGMweCaIFDBZNwhFOFF4FhgXaPGQmFRBIjgQwJgjEcgVQ8MYJIAQEB X-IronPort-AV: E=Sophos;i="5.13,641,1427752800"; d="scan'208";a="166107243" Received: from mail-ig0-f172.google.com ([209.85.213.172]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Jun 2015 00:26:01 +0200 Received: by igbqq3 with SMTP id qq3so2752047igb.0 for ; Thu, 18 Jun 2015 15:26:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=F/fbXRK8zN1BzgximhkHDLT8AZBOZegHoQpz26JT9Wc=; b=lHFyLx64FWLEjXvpXblnENoqRFj9fl32ypHEGcCfrrbz978Cy9MB/Es2MwyDHV1UME vpnEncTv5aGeJHbxa068P12QAs69A94Um1ZitggCQm6YN/qUYlkaWro+L5OoevPvqRjK NWxn7TNnx/trAQZUNft8mI/UurkgIHf3PUJAaBZxYi3U2pfcaqgXo6Nr1RyXbrZqrCX8 tI3aWpeYb8AHulbFBfDcEwUdGmPUCyq0XHiWxNNSXy4kuGSXjNGpDF9Lk+CxrZotPIhi zZHnOjbtTnzb4VCJZSx2u+tPGnlg4bGukAydq+tuwVZN29c7xj3UtSOqMESRX0VRQyGQ BKXA== X-Received: by 10.42.190.129 with SMTP id di1mr4486649icb.11.1434666360537; Thu, 18 Jun 2015 15:26:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.92.131 with HTTP; Thu, 18 Jun 2015 15:25:20 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 19 Jun 2015 00:25:20 +0200 Message-ID: To: Kenneth Adam Miller Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Compilation semantics for static garbage collection You may interested in the Mezzo programming language, a research language developed with the idea of having a finer-grained type-level control of mutable memory. http://protz.github.io/mezzo/ Many of the ideas that are informal in Rust are formally explicited in Mezzo. The language is less ambitious than Rust in terms of feature coverage (and thus less practical for everyday programming), but comes with a precise semantics (which Rust lacks for now) and soundness proof. It is a fairly interesting design, which can be presented as aiming to turn the current research on separation logic into a relatively usable programming language design. For a lively discussion of some of Mezzo design choices, what worked and what did not work so well, see "A few lessons from the Mezzo project", Fran=C3=A7ois Pottier, Jonathan Protzenko, 2015 http://gallium.inria.fr/~fpottier/publis/fpottier-protzenko-lessons-mezzo= .pdf On Thu, Jun 18, 2015 at 9:44 PM, Kenneth Adam Miller wrote: > I was thinking that while rust is new, some of what it is pioneering is > really interesting, especially with the way it deals with ownership being= a > type. Rust doesn't have a GC, yet it rules out leakage and remains fast. = It > also manages concurrency safety very well. > > The stipulations put on types in the ocaml language are pretty strict, and > the GC is transparent to the user. What is the possibility that there cou= ld > ever be a version of ocaml that makes use of something like ownership or > some typing mechanism to determine more at compile time, to facilitate the > removal or reduction of the GC?