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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 9ED8F7EEBF for ; Fri, 19 Jun 2015 04:00:35 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of kennethadammiller@gmail.com) identity=pra; client-ip=209.85.214.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of kennethadammiller@gmail.com designates 209.85.214.180 as permitted sender) identity=mailfrom; client-ip=209.85.214.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f180.google.com) identity=helo; client-ip=209.85.214.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-ob0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CxAgALd4NVlLTWVdFcFoNOXwaDGKklkQ2CG4V2AiiBDQdMAQEBAQEBEgEBAQEHCwsJHzCEGggBAQECAQESER0BGx0BAwELBgUEBw0qAgIhAQERAQUBHBkihVGCJgEDCggNoTg+MYs/gWuCeYs1ChknDVeFDgEBAQEBBQEBAQEBARYBBQ6LN4JNgjkHgmgPgTQFk3SEVIUXgWGBdo8bCYVEEiOBDAkRBoIaHIFuIjEBgkcBAQU X-IPAS-Result: A0CxAgALd4NVlLTWVdFcFoNOXwaDGKklkQ2CG4V2AiiBDQdMAQEBAQEBEgEBAQEHCwsJHzCEGggBAQECAQESER0BGx0BAwELBgUEBw0qAgIhAQERAQUBHBkihVGCJgEDCggNoTg+MYs/gWuCeYs1ChknDVeFDgEBAQEBBQEBAQEBARYBBQ6LN4JNgjkHgmgPgTQFk3SEVIUXgWGBdo8bCYVEEiOBDAkRBoIaHIFuIjEBgkcBAQU X-IronPort-AV: E=Sophos;i="5.13,641,1427752800"; d="scan'208";a="136910925" Received: from mail-ob0-f180.google.com ([209.85.214.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Jun 2015 04:00:34 +0200 Received: by obbsn1 with SMTP id sn1so65851995obb.1 for ; Thu, 18 Jun 2015 19:00:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:cc :content-type; bh=SnSffEgwTVzr6LhNXsViFlkqCVq89iKMn+cf+fFbuBk=; b=iH09jR3xvgcH+uee36OzPX+Gf1/0UOuCdlzhbJvPuLaR2La1/pF50ekZuzpiqQPdCy Ql6cak5ah1S1/tdDSntNDReNlnkwObkfwYcw/A7Y/PPLceOUrUaBA2iLJ21RHT1OWCrV 08DNUoig39DW+QxHyruLRg++QnjhH/yA+Wm+brLGqb8SffflgqWEvmlMUa0DB/adBFO3 y9q4nMi+nZk4LORJ9W/lPQg33LbeiKeyOpdVM7Y75/iWjYRSa0L1T4K2KPr7hv9sNhEy ueqGJrx56c891gOXcuRnIiSpnWk8nud0fKLhhnGmxrP0VLobB0PLTA0ZmIdsSxFXV7Io CdAQ== MIME-Version: 1.0 X-Received: by 10.60.35.8 with SMTP id d8mr11568192oej.37.1434679232745; Thu, 18 Jun 2015 19:00:32 -0700 (PDT) Received: by 10.202.191.8 with HTTP; Thu, 18 Jun 2015 19:00:32 -0700 (PDT) In-Reply-To: References: Date: Thu, 18 Jun 2015 22:00:32 -0400 Message-ID: From: Kenneth Adam Miller Cc: caml users Content-Type: multipart/alternative; boundary=089e013cc15408d5f00518d54ac3 Subject: Re: [Caml-list] Compilation semantics for static garbage collection --089e013cc15408d5f00518d54ac3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks to all! I appreciate the enlightenment. I think I did a poor job on my word selection, a regular from me. On Thu, Jun 18, 2015 at 6:25 PM, Gabriel Scherer wrote: > 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 > could > > 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? > --089e013cc15408d5f00518d54ac3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Thanks to all! I appreciate the enlightenment. I think I d= id a poor job on my word selection, a regular from me.=C2=A0

On Thu, Jun 18, 2015 at 6:= 25 PM, Gabriel Scherer <gabriel.scherer@gmail.com> w= rote:
You may interested in the Mezzo pro= gramming language, a research
language developed with the idea of having a finer-grained type-level
control of mutable memory.
=C2=A0 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
=C2=A0 "A few lessons from the Mezzo project",
=C2=A0 Fran=C3=A7ois Pottier, Jonathan Protzenko, 2015
=C2=A0 http://gallium.i= nria.fr/~fpottier/publis/fpottier-protzenko-lessons-mezzo.pdf

On Thu, Jun 18, 2015 at 9:44 PM, Kenneth Adam Miller
<kennethadammiller@gmail.= com> wrote:
> I was thinking that whi= le rust is new, some of what it is pioneering is
> really interesting, especially with the way it deals with ownership be= ing 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 = could
> 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?

--089e013cc15408d5f00518d54ac3--