I am not sure it is the right place to ask this, but: is the analog of Featherweight Java had been define for Rust ?
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.
You may be interested in e.g. sealed rust
As far as I know sealed rust is still a concept.
yes, though there's active work on it
This is exactly what I was thinking about ! Thanks.
one of the authors, Niko Matsakis, is in this chat - you can talk to them if you wish.
That's even better. Many thanks.
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.
@Aaron Weiss, another author of that paper, is also here in this chat and might know ;)
and btw I'm one of the authors of the rustbelt paper mentioned above
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.
that sounds like a fun project :D
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.