2019/07/25 by Dimitri Racordon, Racordon, Dimitri, Didier Buchs +1
Computer Science · #D.3.3 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1907.11317
openalex publication_date 2019/07/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.