Formal Semantics / Type Rules


I’ve pestered some people over twitter about this and they let me know (a while ago and then again today) that it’s “in the works”.

I guess I’d be interested in contributing if I can find the time so I was curious if anyone has started on setting out the formal semantics and type rules for Rust? I’ve only ever done semantics with paper/pencil and LaTeX so maybe some tooling is appropriate here (PLT Redex, twelf)?



Niko has a redex model that I know he’s used to prototype some features – I believe DST.

I think there are a couple of other existing models as well. Eric Reed at the University of Washington has been working on this, in particular, but I don’t know the status.


@aturon Great! I can take a look at the redex definition to educate myself at least. Thanks very much for pointing me to Eric Reed as well.