Towards a Synthesis

Previous approaches that formalize Rust ownership, borrowing:

  • RustBelt (includes pointer arithmetic, unsafe) (Ralf Jung et al.)
  • Featherweight Rust (David Pearce)

Goal:

  • isolate how ownership relates to linear logic / bunched implications
  • choose subset of Rust that is easily recognized
  • canonical way to "translate away" flow (CPS)

What follows are early ideas how this might look.