Re: [Caml-list] Compilation semantics for static garbage collection

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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çois 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
<kennethadammiller@gmail.com> 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?