Stream: wg-formal-methods

Topic: Featherweight Rust


Nicolas Osborne (Apr 17 2020 at 12:32, on Zulip):

Hello everyone,
I am not sure it is the right place to ask this, but: is the analog of Featherweight Java had been define for Rust ?

bjorn3 (Apr 17 2020 at 12:43, on Zulip):

https://plv.mpi-sws.org/rustbelt/

Nicolas Osborne (Apr 17 2020 at 12:58, on Zulip):

Yes, this is a fascinating project. But if I remember correctly, they define Lambda-Rust which is a separation logic and is expressed in continuation passing style. I was thinking of a language close to Rust but with less features.

simulacrum (Apr 17 2020 at 13:01, on Zulip):

You may be interested in e.g. sealed rust

bjorn3 (Apr 17 2020 at 13:03, on Zulip):

As far as I know sealed rust is still a concept.

simulacrum (Apr 17 2020 at 13:03, on Zulip):

yes, though there's active work on it

Nicolas Osborne (Apr 17 2020 at 13:04, on Zulip):

This is exactly what I was thinking about ! Thanks.

Vytautas Astrauskas (Apr 18 2020 at 15:29, on Zulip):

https://arxiv.org/pdf/1903.00982.pdf

Shnatsel (Apr 18 2020 at 15:33, on Zulip):

one of the authors, Niko Matsakis, is in this chat - you can talk to them if you wish.

Nicolas Osborne (Apr 18 2020 at 15:47, on Zulip):

That's even better. Many thanks.

RalfJ (Apr 19 2020 at 07:46, on Zulip):

Note though that that paper contains some flaws (it's a preprint, not a reviewed published paper). the authors are working on a significantly improved next version. not sure if that is already available somewhere.

RalfJ (Apr 19 2020 at 07:47, on Zulip):

@Aaron Weiss, another author of that paper, is also here in this chat and might know ;)

RalfJ (Apr 19 2020 at 07:48, on Zulip):

and btw I'm one of the authors of the rustbelt paper mentioned above

Nicolas Osborne (Apr 19 2020 at 10:44, on Zulip):

I really enjoyed the rustbelt paper (I didn't understand all of it, I have to work a bit more :-) )

In the context of the compilation course for my master degree, I am implementing something like a borrow-checker. But, on the side, I am interested in investigating whether it is possible to implement a compilator "correct by construction" for a very little language (like Imp in Software Foundations) in Agda. (Here, correct means with semantic preservation).

For now, I am just experimenting in expressing syntax and semantics. The first step would be to have a type-checker correct by construction like what did McBride and McKinna for the simply typed lambda calculus in The view from the left. So, I am drawn in puting more features in the language like functions and affine type system.

RalfJ (Apr 19 2020 at 11:26, on Zulip):

that sounds like a fun project :D

Aaron Weiss (Apr 20 2020 at 15:15, on Zulip):

RalfJ said:

Aaron Weiss, another author of that paper, is also here in this chat and might know ;)

I am indeed here, and happy to answer any questions. There has indeed been a lot of fixes to Oxide since that draft was uploaded, but I will hopefully be uploading a new (and hopefully much-improved) draft in the next few weeks.

Last update: Jun 05 2020 at 23:00UTC