pith. sign in

arxiv: 1907.11317 · v1 · pith:LJ7WOS7Inew · submitted 2019-07-25 · 💻 cs.PL

Explicit and Controllable Assignment Semantics

Dimitri Racordon , Didier Buchs This is my paper

Pith reviewed 2026-05-24 15:28 UTC · model grok-4.3

classification 💻 cs.PL
keywords assignment semanticsprogramming language designtype capabilitiesuniquenessimmutabilityimperative programmingformal semanticsminimal calculus
0
0 comments X

The pith

Anzen supplies three assignment operators with unequivocal semantics that reproduce every common imperative strategy, backed by a capability type system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Anzen to remove relics of implicit memory models that make assignment confusing in most languages. It defines three operators whose meanings stay fixed and sufficient to express all standard patterns such as copy, move, and reference. A type system built on capabilities tracks uniqueness and immutability so that intent is enforced statically. The design is presented informally and then captured exactly in a minimal calculus. A reader would care because clearer assignment reduces the gap between what a programmer writes and what the machine actually does.

Core claim

Anzen provides three assignment operators with unequivocal semantics that can reproduce all common imperative assignment strategies. It is accompanied by a type system based on type capabilities to enforce uniqueness and immutability. The language and its rules are formalized by means of a minimal calculus.

What carries the argument

Three assignment operators with fixed, explicit semantics together with a type-capability system that tracks uniqueness and immutability.

If this is right

  • Every standard imperative assignment pattern becomes expressible with one of the three operators.
  • Uniqueness and immutability constraints are checked by the type system rather than left to runtime or convention.
  • The minimal calculus supplies a precise reference for any future implementation or proof.
  • Code can convey assignment intent without relying on hidden details of the memory model.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Other language features that currently hide memory effects could be made explicit using similar operator sets.
  • The capability mechanism might be applied to additional properties such as aliasing in concurrent code.
  • Empirical measurement of developer error rates on assignment tasks could test whether the explicit operators reduce mistakes in practice.

Load-bearing premise

That the three operators and the capability type system can be implemented at full scale without creating new sources of confusion or unsoundness.

What would settle it

A realistic program whose intended assignment behavior cannot be expressed using only the three operators without producing an outcome the programmer did not expect.

Figures

Figures reproduced from arXiv: 1907.11317 by Didier Buchs, Dimitri Racordon.

Figure 1
Figure 1. Figure 1: Effect of bitwise copy assignment. Two local vari￾ables x and y are assigned to two other local variables a and b, respectively. The variable a represents a number allocated on the stack. It is copied during x’s assignment, which there￾fore represents a different object. On the other hand, since b represents a tree allocated on the heap, its pointer is copied during y’s assignment, resulting in an alias. U… view at source ↗
Figure 2
Figure 2. Figure 2: Effect of assignment operators. Each illustration depicts the situations before and after a particular assign￾ment, starting from a state where two variables a and b are bound to unrelated memory locations, holding the values 8 and 4 respectively. Changes are highlighted in color [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
read the original abstract

Despite the plethora of powerful software to spot bugs, identify performance bottlenecks or simply improve the overall quality of code, programming languages remain the first and most important tool of a developer. Therefore, appropriate abstractions, unambiguous syntaxes and intuitive semantics are paramount to convey intent concisely and efficiently. The continuing growth in computing power has allowed modern compilers and runtime system to handle once thought unrealistic features, such as type inference and reflection, making code simpler to write and clearer to read. Unfortunately, relics of the underlying memory model still transpire in most programming languages, leading to confusing assignment semantics. This paper introduces Anzen, a programming language that aims to make assignments easier to understand and manipulate. The language offers three assignment operators, with unequivocal semantics, that can reproduce all common imperative assignment strategies. It is accompanied by a type system based on type capabilities to enforce uniqueness and immutability. We present Anzen's features informally and formalize it by the means of a minimal calculus.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces Anzen, a language featuring three distinct assignment operators with unequivocal semantics capable of reproducing common imperative assignment strategies (e.g., copy, move, reference). These are paired with a capability-based type system to enforce uniqueness and immutability properties. The features are first described informally and then formalized via a minimal calculus.

Significance. If the minimal calculus is sound, the work provides a clean, explicit design for assignment that addresses longstanding sources of confusion in imperative languages. The capability type system offers a lightweight mechanism for static enforcement of aliasing and mutability constraints. The scoping of claims exactly to the minimal calculus (rather than full-language implementation) is a strength, as is the absence of ad-hoc parameters or fitted quantities.

minor comments (2)
  1. The informal presentation would benefit from a side-by-side comparison table showing how each of the three operators maps to common patterns in languages such as C++ and Java.
  2. Notation for the capability types (e.g., the exact syntax for uniqueness and immutability annotations) should be introduced with a small grammar fragment before the first use in the informal section.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review and recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity; design contribution is self-contained

full rationale

The paper introduces a new language design (Anzen) with three assignment operators and a capability-based type system, formalized via a minimal calculus. No equations, fitted parameters, or predictions appear that reduce to inputs by construction. No self-citations are load-bearing for any central claim, and the work does not invoke uniqueness theorems or ansatzes from prior author work. The central claim is scoped exactly to the informal description plus minimal calculus, making the derivation self-contained without reduction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are identifiable from the abstract alone.

pith-pipeline@v0.9.0 · 5685 in / 982 out tokens · 20961 ms · 2026-05-24T15:28:10.380735+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Björn Andrist and Viktor Sehr. 2018. C++ High Performance . Packt Publishing, Birmingham, United Kingdom

    work page 2018

  2. [2]

    Gavin M Bierman, MJ Parkinson, and AM Pitts. 2003. MJ: An imper- ative core calculus for Java and Java with effects . Technical Report. Explicit and Controllable Assignment Semantics MPLR’2019, O ctober 20–25, 2019, Athens, Greece University of Cambridge, Computer Laboratory

    work page 2003

  3. [3]

    John Boyland. 2003. Checking Interference with Fractional Per- missions. In Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings . 55–72. h/t_tps://doi.org/10.1007/3-540-44898-5_4

    work page doi:10.1007/3-540-44898-5_4 2003

  4. [4]

    John Boyland, James Noble, and William Retert. 2001. Capa- bilities for Sharing: A Generalisation of Uniqueness and Read- Only. In ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedi ngs. 2–27. h/t_tps://doi.org/10.1007/3-540-45337-7_2

    work page doi:10.1007/3-540-45337-7_2 2001

  5. [5]

    Andrea Capriccioli, Marco Servetto, and Elena Zucca. 2016. An I mper- ative Pure Calculus. Electronic Notes in Theoretical Computer Science 322 (2016), 87–102. h/t_tps://doi.org/10.1016/j.entcs.2016.03.007

    work page doi:10.1016/j.entcs.2016.03.007 2016

  6. [6]

    Kung Chen and Martin Odersky. 1994. A Type System for a Lambda Calculus with Assignments. In Theoretical As- pects of Computer Software, International Conference TACS ’94, Sendai, Japan, April 19-22, 1994, Proceedings . 347–364. h/t_tps://doi.org/10.1007/3-540-57887-0_103

    work page doi:10.1007/3-540-57887-0_103 1994

  7. [7]

    Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. 2013. Ownership Types: A Survey. In Aliasing in Object-Oriented Programming. Types, Analysis and Verifi - cation. Springer Berlin Heidelberg, Berlin, Heidelberg, 15–58. h/t_tps://doi.org/10.1007/978-3-642-36946-9_3

    work page doi:10.1007/978-3-642-36946-9_3 2013

  8. [8]

    Ana Lúcia de Moura and Roberto Ierusalimschy. 2009. Revisiting coroutines. ACM Transactions on Programming Languages and Sys- tems 31, 2 (2009), 6:1–6:31. h/t_tps://doi.org/10.1145/1462166.1462167

    work page doi:10.1145/1462166.1462167 2009

  9. [9]

    Werner Dietl, Sophia Drossopoulou, and Peter Müller. 2011. S epa- rating ownership topology and encapsulation with generic universe types. ACM Transactions on Programming Languages and Systems 33, 6 (2011), 20:1–20:62. h/t_tps://doi.org/10.1145/2049706.2049709

    work page doi:10.1145/2049706.2049709 2011

  10. [10]

    Friedman

    Matthias Felleisen and Daniel P. Friedman. 1989. A Syntactic The- ory of Sequential State. Theor. Comput. Sci. 69, 3 (1989), 243–287. h/t_tps://doi.org/10.1016/0304-3975(89)90069-8

    work page doi:10.1016/0304-3975(89)90069-8 1989

  11. [11]

    Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen

    work page

  12. [12]

    In POPL ’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998

    Classes and Mixins. In POPL ’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998 . 171–183. h/t_tps://doi.org/10.1145/268946.268961

    work page doi:10.1145/268946.268961 1998

  13. [13]

    Paola Giannini, Marco Servetto, and Elena Zucca. 2018. A Syntactic Model of Mutation and Aliasing. In Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Inter- section Types and Related Systems, DCM/ITRS 2018, and Ninth Work- shop on Intersection Types and Related Systems Oxford, UK, 8 th July

    work page 2018

  14. [14]

    h/t_tps://doi.org/10.4204/EPTCS.293.4

    39–55. h/t_tps://doi.org/10.4204/EPTCS.293.4

    work page doi:10.4204/eptcs.293.4

  15. [15]

    Gordon, Matthew J

    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Br om- field, and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Lang uages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, Oc- tober 21-25, 2012. 21...

    work page doi:10.1145/2384616.2384619 2012

  16. [16]

    Steele, Gilad Bracha, Alex Bu ckley, and Daniel Smith

    James Gosling, Bill Joy, Guy L. Steele, Gilad Bracha, Alex Bu ckley, and Daniel Smith. 2019. The Java Language Specification, Java SE 12 Edition

    work page 2019

  17. [17]

    Pierce, and Philip Wadler

    Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Feath- erweight Java: a minimal core calculus for Java and GJ. ACM Trans- actions on Programming Languages and Systems 23, 3 (2001), 396–450. h/t_tps://doi.org/10.1145/503502.503505

    work page doi:10.1145/503502.503505 2001

  18. [18]

    Levy, Michael P

    Amit A. Levy, Michael P. Andersen, Bradford Campbell, David E . Culler, Prabal Dutta, Branden Ghena, Philip Levis, and Pat Pannuto

    work page

  19. [19]

    In Proceedings of the 8th Workshop on Programming Languages and Operating Systems, PLOS 2015, Monterey, California, US A, October 4, 2015

    Ownership is theft: experiences building an embedded OS in rust. In Proceedings of the 8th Workshop on Programming Languages and Operating Systems, PLOS 2015, Monterey, California, US A, October 4, 2015. 21–26. h/t_tps://doi.org/10.1145/2818302.2818306

    work page doi:10.1145/2818302.2818306 2015

  20. [20]

    Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas Robert Cameron. 2012. Encoding Featherweight Java with assignment and immutability using the Coq proof assis- tant. In Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP 2012, Beijing, China, June 12, 20 12. 11–19. h/t_tps://doi.org/10.1145/2318202.2318206

    work page doi:10.1145/2318202.2318206 2012

  21. [21]

    Jeff Meyerson. 2014. The Go Programming Language. IEEE Software 31, 5 (2014), 104. h/t_tps://doi.org/10.1109/MS.2014.127

    work page doi:10.1109/ms.2014.127 2014

  22. [22]

    Robin Milner. 1978. A Theory of Type Polymorphism in Program- ming. Journal of Computer System and Sciences 17, 3 (1978), 348–375. h/t_tps://doi.org/10.1016/0022-0000(78)90014-4

    work page doi:10.1016/0022-0000(78)90014-4 1978

  23. [23]

    Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierho ff

    work page

  24. [24]

    In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, Ja nuary 22- 28, 2012

    A type system for borrowing permissions. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, Ja nuary 22- 28, 2012. 557–570. h/t_tps://doi.org/10.1145/2103656.2103722

    work page doi:10.1145/2103656.2103722 2012

  25. [25]

    Martin Odersky, Dan Rabin, and Paul Hudak. 1993. Call by Name , As- signment, and the Lambda Calculus. In Conference Record of the Twen- tieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Pro- gramming Languages, Charleston, South Carolina, USA, Janu ary 1993. 43–56. h/t_tps://doi.org/10.1145/158511.158521

    work page doi:10.1145/158511.158521 1993

  26. [26]

    Emmanuel Paraids. 2002. R for Beginners

    work page 2002

  27. [27]

    Alex Potanin, Monique Damitio, and James Noble. 2013. Are your incoming aliases really necessary? counting the cost of ob- ject ownership. In 35th International Conference on Software Engi- neering, ICSE ’13, San Francisco, CA, USA, May 18-26, 2013 . 742–751. h/t_tps://doi.org/10.1109/ICSE.2013.6606620

    work page doi:10.1109/icse.2013.6606620 2013

  28. [28]

    Alex Potanin, Johan Östlund, Yoav Zibin, and Michael D. Ernst

    work page

  29. [29]

    In Aliasing in Object-Oriented Programming

    Immutability. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification. Springer Berlin Heidelberg, 233–269. h/t_tps://doi.org/10.1007/978-3-642-36946-9_9

    work page doi:10.1007/978-3-642-36946-9_9

  30. [30]

    Dimitri Racordon and Didier Buchs. 2018. A practical type system for safe aliasing. In Proceedings of the 11th ACM SIG- PLAN International Conference on Software Language Engine er- ing, SLE 2018, Boston, MA, USA, November 05-06, 2018 . 133–146. h/t_tps://doi.org/10.1145/3276604.3276612

    work page doi:10.1145/3276604.3276612 2018

  31. [31]

    Strom and Shaula Yemini

    Robert E. Strom and Shaula Yemini. 1986. Typestate: A Pro- gramming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering 12, 1 (1986), 157–171. h/t_tps://doi.org/10.1109/TSE.1986.6312929

    work page doi:10.1109/tse.1986.6312929 1986

  32. [32]

    Phit-Huan Tan, Choo-Yee Ting, and Siew-Woei Ling. 2009. Learning Difficulties in Programming Courses: Undergraduates’ Perspective and Perception. In 2009 International Conference on Computer Technol- ogy and Development (ICCTD), Kota Kinabalu, Malaysia, Vol. 1. 42–46. h/t_tps://doi.org/10.1109/ICCTD.2009.188

    work page doi:10.1109/icctd.2009.188 2009

  33. [33]

    Akihiko Tozawa, Michiaki Tatsubori, Tamiya Onodera, and Yasuhik o Minamide. 2009. Copy-on-write in the PHP language. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Pr o- gramming Languages, POPL 2009, Savannah, GA, USA, January 2 1-23,

    work page 2009

  34. [34]

    h/t_tps://doi.org/10.1145/1480881.1480908

    200–212. h/t_tps://doi.org/10.1145/1480881.1480908

    work page doi:10.1145/1480881.1480908

  35. [35]

    Josuttis

    David Vandevoorde and Nicolai M. Josuttis. 2002. C++ Templates: The Complete Guide, Portable Documents . Addison-Wesley, Boston, MA, United States

    work page 2002

  36. [36]

    Jan Vitek and Boris Bokowski. 2001. Confined types in Java. Software: Practice and Experience 31, 6 (2001), 507–532. h/t_tps://doi.org/10.1002/spe.369

    work page doi:10.1002/spe.369 2001

  37. [37]

    Philip Wadler. 1990. Linear Types can Change the World!. In Program- ming concepts and methods: Proceedings of the IFIP Working G roup 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel. 561

    work page 1990

  38. [38]

    Hongseok Yang and Uday Reddy. 1997. Imperative lambda calcu- lus revisited . Technical Report. University of Illinois at Urbana- Champaign

    work page 1997