Native Implementation of Mutable Value Semantics
Dimitri Racordon, Denys Shabalin, Daniel Zheng, Dave Abrahams, and Brennan Saeta

TL;DR
This paper presents a native implementation of mutable value semantics, a programming approach that avoids shared mutable state by banning sharing, supporting in-place mutation, and maintaining a simple type system, with an efficient compilation strategy.
Contribution
It introduces a language design with mutable value semantics and demonstrates how to compile it to efficient native code using stack allocation and runtime optimizations.
Findings
Efficient native code compilation achieved for mutable value semantics.
Supports in-place mutation without sharing mutable state.
Maintains a simple type system while enabling mutable references.
Abstract
Unrestricted mutation of shared state is a source of many well-known problems. The predominant safe solutions are pure functional programming, which bans mutation outright, and flow sensitive type systems, which depend on sophisticated typing rules. Mutable value semantics is a third approach that bans sharing instead of mutation, thereby supporting part-wise in-place mutation and local reasoning, while maintaining a simple type system. In the purest form of mutable value semantics, references are second-class: they are only created implicitly, at function boundaries, and cannot be stored in variables or object fields. Hence, variables can never share mutable state. Because references are often regarded as an indispensable tool to write efficient programs, it is legitimate to wonder whether such a discipline can compete other approaches. As a basis for answering that question, we…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Formal Methods in Verification
