[Caml-list] Compilation semantics for static garbage collection

[Caml-list] Compilation semantics for static garbage collection

[Kenneth Adam Miller]

[-- Attachment #1: Type: text/plain, Size: 599 bytes --]

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?

[-- Attachment #2: Type: text/html, Size: 638 bytes --]

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

[Malcolm Matalka]

Kenneth Adam Miller <kennethadammiller@gmail.com> writes:

> 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?

From my understanding, Rust is just doing linear typing.  There is an ML
variant called LinearML from Anil that implements this, but it's a toy.
This could be added to Ocaml, but I think it's really unclear how it
would interact with the rest of the language.

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

[Gabriel Scherer]

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?

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

[Kenneth Adam Miller]

[-- Attachment #1: Type: text/plain, Size: 1945 bytes --]

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 <gabriel.scherer@gmail.com>
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ç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?
>

[-- Attachment #2: Type: text/html, Size: 2671 bytes --]