The Mutable Value Semantics (MVS): A Non-superficial Study
This is the first post in the Eter programming language series. Although part of this series, it is not part of the Eter language itself. The Eter language is currently in the design and development phase, and this series (including this post) should be considered an exploration of ideas that will serve as a foundation for the language. No prior knowledge of Eter, or of its motivations, is required to read these early posts. However, if you are interested in the project, you can find more information in the Eter compiler monorepo. The Eter language reference and the Eter Doxygen documentation, although not yet complete, are also good starting points.
Overall, we are currently researching:
- a novel semantics for a system programming language inspired by the Ownership and Borrowing model (Affine Type Systems with Lifetimes) and the Mutable Value Semantics (MVS),
- mechanisms to integrate Machine Learning (ML) and Deep Learning (DL) models as first-class entities in the language (e.g., via simple extern functions),
- support for seamless coexistence between CPU and GPU computations (similar to the Mojo programming language ), and
- a tile-level programming model for GPU computation, inspired by systems such as NVIDIA's Tile IR , Triton , Triton-based Gluon , Halide , and related approaches such as Tilus .
But for now, let's put aside everything that Eter is supposed to be...
Introduction
It is fair to say that one of the most important aspects in the design of a programming language is its semantics—particularly its memory model. The memory model describes how the language behaves when memory is manipulated, whether manually or automatically. This includes aliasing rules, thread visibility, and the ordering of memory operations (such as atomicity).
More fundamentally, the memory model defines what it means for a program to be safe, by specifying which behaviors are well-defined and which fall into undefined behavior (UB). Ensuring that safe programs cannot violate these constraints is the responsibility of the language's type system and static analyses.
Ideally, we would like to eliminate undefined behavior altogether—at least for a meaningful and practical subset of the language.1
The Mutable Value Semantics (MVS)
Racordon et al. introduced Mutable Value Semantics (MVS) as a novel semantics for a system programming language that aims to address the challenges of memory safety and concurrency.2 MVS is a programming discipline that advocates for value independence to support local reasoning. In its strictest form, references are second-class elements: they are created only implicitly, at function boundaries, and cannot be stored in variables or object fields. Therefore, variables can never share a mutable state. Unlike pure functional programming, however, mutable value semantics allows partial in-place mutation, eliminating the memory traffic typically associated with functional updates of immutable data.
In the following, we will use a programming language with simple features (called Swiftlet) to illustrate the concepts of value semantics. This analysis draws heavy inspiration from the original paper; for a more formal and exhaustive treatment of the topic, I highly recommend referring to their work. As all types have value semantics, values form disjoint topological trees rooted at variables or constants. All function parameters are passed by value, and all function results are returned by value. Therefore, the following code is well-typed:
struct Vec2 { ... };
var v = Vec2(x: 1, y: 2);
var u = v;
u.y = 3 // `v` -> Vec2(x: 1, y: 2)
// `u` -> Vec2(x: 1, y: 3)
Conceptually, the line 3 can be always viewed as a copy of the value of v (optimizations are possible).
On the other hand, the following code is ill-typed due to the immutable property of v:
struct Vec2 { ... };
let v = Vec2(x: 1, y: 2);
v.x = 3 // ERROR: `v` is immutable
To implement in-place part-wise mutation the inout keyword is used.
For instance, the following code is well-typed:
struct Vec2 { ... };
func move_x(v: inout Vec2, x: Int) -> Void {
v.x = v.x + d;
};
var v = Vec2(x: 1, y: 2);
_ = move_x(&v, x: 3);
// `v` -> Vec2(x: 4, y: 2)
Conceptually, line 6 can be viewed as a copy of the value of v,
then a copy back to v,
after move_x is called.
As the paper presents MVS, the inout keyword can only be used for
formal parameters—we cannot initialize or assign an inout variable, a
limitation overcome by Hylo.
Multiple inout formal parameters are allowed as long as at the
call site
the actual parameters are all disjoint trees, i.e., they do not share any part of their value.
For instance, the following code is well-typed:
struct Vec2 { ... };
func move_xy(x: inout Int, y: inout Int, inc: Int) -> Void {
x = x + inc;
y = y + inc;
};
var v = Vec2(x: 1, y: 2);
_ = move_xy(&v.x, &v.y, inc: 3)
// `v` -> Vec2(x: 4, y: 5)
This Law of Exclusivity states that a value cannot be
simultaneously owned by two different owners.
In other words, a value cannot be shared between multiple owners.
For instance, the following code is ill-typed because the x is shared
twice:
the first time at the call site when it is passed as an inout parameter
and the second time when it is captured by the g function
(similar to Linear Type System).
var x = 0;
func g(y: inout Int) { y += x };
g (y: &x) // ERROR: `x` is shared twice
Both Swift and Hylo (formerly Val) adopt this model but in different ways. Swift tries to make values look like safe references, while Hylo treats everything as a pure value, eliminating the need for a Garbage Collector (GC) or Atomic Reference Counting (ARC).
Possible Optimizations?
The Move Semantics. A recurring pattern is to assign values just after they have been created. For instance:
func f(a: [Int]) { ... };
var x = [1,2,3];
f(x)
A simple implementation would evaluate the right operand (the rvalue [1,2,3]), copy this value to assign x,
and then destroy the original.
Of course, move semantics comes into play when the rvalue is a temporary. In this case, the compiler
can simply move the value from the rvalue to the lvalue.
Note that the same optimization could be applied on the last use of a value.
However, this is not possible in the general case, as the value could be used in multiple places.
Aliases for copies. All function parameters are passed by value, but the copy is not necessarily performed. Broadly speaking, we can see formal parameters as aliases to values stored at the call site. This holds as long as the lifetime of the formal parameter is not shorter than the lifetime of the actual parameter, just as the Rust immutable borrows . Consider the following example:
func f(a: [Int]) { ... };
var x = [1,2,3];
f(x);
x.append(4);
In this example, the formal parameter a is an alias to the actual
parameter x.
The static analysis must ensure that formal parameters don't escape the call site.
A similar optimization is used in the presence of multiple let bindings.
For instance:
func f(a: [Int]) { ... };
let x = [[1,2,3], [4,5,6]]; // ────────┐
let y = x[0]; // ────┐ │
f(y) // │ │
// `y` dies here // <───┘ │
// `x` dies here // <───────┘
Since the lifetime y is shorter than the
lifetime of x, y
can simply be an alias to the first element of x avoiding the
copy.
Copy-on-write. Aliases for copies are not applicable in the presence of mutation. This is true for both left and right-hand sides of the assignment. In principle, these should be copied, but in practice, the compiler may choose to copy-on-write (CoW) the data at runtime. This is achieved using atomic reference counting (ARC) to track how many owners there are. If the count is greater than 1, a copy is performed. Consider the following example:
func sort (array: inout [Int]) -> Void { ... };
var a0 = [1, 2];
var a1 = a0;
sort(array: &a1)
No copy is performed in the above example, because a0 is already sorted.
Otherwise, if a0 were not sorted (e.g., a0 = [2, 1]), a copy would be performed.
This mechanism introduces latency, as every mutation involves a small ARC check, which can cause overhead in
high-performance contexts.
More importantly, it leads to an unsoundness issue with inout
parameters and interior pointers.
While the following code is expected to compile and run without errors, it is still unsound:
func sort (array: inout [Int]) -> Void { ... };
var a0 = [[1 , 2] , [3 , 4]];
var a1 = a0;
sort(array: &a0[1])
a0 and a1 share the same outer array
storage.
Passing &a0[1] exposes an interior pointer to a subarray within that
shared storage.
Since the callee has no visibility into the aliasing of the enclosing structure, it may perform mutations
under the assumption of uniqueness, potentially violating value semantics.
Leveraging local reasoning. Since the 2000s, local reasoning has been important in the design of programming languages (see O'Hearn et al. ). Consider the following example:
struct Vec2 { ... };
func f (v0: Vec2 ) -> Vec2 {
var v1 = v0;
let v2 = v1;
v1.x = 8;
Vec2(x: v2.x, y: v1.y)
}
Thanks to local reasoning, the compiler can discard the line 5 completely, as it is not an observable side effect of the function. Additionally, the local reasoning can be leveraged by scalar replacement of aggregates (SROA) .
The Swift's Mutable Value Semantics
In Swift, for value types (structs), the MVS is implemented via a CoW mechanism. When you assign an array to a new variable, Swift does not immediately copy the data; both variables point to the same memory. The copy only occurs if one of the instances is modified. This requires hidden ARC to track how many owners there are. If the count is greater than 1, a copy is performed. For instance, the following code is well-typed:
var a = [1, 2, 3] // `a` owns the array
var b = a // `b` shares ownership with `a`, no copy yet
b.append(4) // `b` mutates the array, triggers a copy due to ARC check
print(a) // -> [1, 2, 3]
print(b) // -> [1, 2, 3, 4]
Swift's MVS allows for reference types (classes), which permit aliasing—i.e., multiple variables can point to the same object and mutate it. This violates the Law of Exclusivity introduced above and breaks local reasoning: you can no longer reason about your code by looking only at the local scope, because an alias might be mutated elsewhere—leading to subtle bugs if not used carefully.
This lack is further exacerbated by the fact that, in Swift, the example we introduced earlier compiles
without
errors, but
crashes at runtime (Compiler explorer) since x is shared twice:
var x = 0;
func g(y: inout Int) { y += x }
g (y: &x)
The Hylo's Mutable Value Semantics
Hylo takes a more radical approach to MVS. It removes CoW in favor of an ownership model where values are truly independent and an in-place mutation semantics that allows for efficient updates without copying. The language statically guarantees that there are no shared mutable references, eliminating the need for a GC or ARC. Consider the following Hylo code:
fun main() {
let weight = 1.0
let base_length = 2.0
var length = base_length // <----------------------------------------------------+
&length += 3.0 // |
let measurements = ( // |
w: weight, // <-----------------------------------------------+ |
l: length) // | |
print(weight) // error: `weight` used after being consumed here -+ |
// |
print(base_length) // error: `base_length` used after being consumed here -+
}
The error occurs because the values of both weight and base_length are used after they have been consumed. In this case, Hylo's
ownership model ensures that the values are truly independent and that there are no shared mutable
references.
Hylo has no reference types but allows, via inout and sink, for efficient mutation without copying. Consider the following Hylo
code:
var point = (x: 0.0, y: 1.0) // `point` owns the tuple
inout x = &point.x // `x` is a mutable reference to `point.x`, no copy, but safe due to ownership rules
&x = 3.14 // Mutating `x` updates `point.x` directly, no copy, and safe due to ownership rules
print(point) // Output: (x: 3.14, y: 1.0)
In this example, the inout keyword creates a "mutable reference" to
point.x, allowing efficient mutation without copying. To show the sink keyword, consider:
fun offset_sink(_ base: sink Vector2, by delta: Vector2) -> Vector2 {
&base.x += delta.x
&base.y += delta.y
return base // Escaping the sink value allows it to be returned without copying,
// as ownership is transferred to the caller
}
fun main() {
let v = (x: 1, y: 2)
print(offset_sink(v, (x: 3, y: 5))) // Output: (x: 4, y: 7)
print(v) // Error: `v` has been moved and cannot be used after being passed as a sink
}
This example shows how to use the sink keyword to create a "sink" value
that can be passed to a function without copying. The function offset_sink takes a sink value and
returns a new value. Ownership is transferred to the caller, which can then use it without copying. A
parallelism between Hylo, Rust, and C++ is provided by the Hylo documentation3.
Hylo has both immutable and mutable projections. The following code shows how to use them:
fun f1() {
var x = 42
inout y = x // mutable projection begins here
print(x) // ERROR: `x` is projected mutably
x += 1 // ERROR: `x` is projected mutably
print(y) // mutable projection ends afterward
}
fun f2() {
var x = 42
let y = x // immutable projection begins here
print(x) // OK
x += 1 // error: `x` is projected immutably
print(y) // immutable projection ends afterward
}
The first function f1 shows how to use a mutable projection. The
compiler prevents the mutation of the value after the mutable projection. The second function f2 shows how to use an immutable projection. The compiler prevents the
mutation of the value after the immutable projection.
A peculiarity of Hylo is that by writing the f2 function as follows:
fun f2() {
var x = 42
let y = x // immutable projection begins here
print(x) // OK
print(y) // immutable projection ends here
x += 1 // OK because the compiler knows that `y` is not longer used
}
The compiler is able to infer that the value of y is not used after the
immutable projection, and therefore the mutation of x is safe.
Rust vs Hylo
To show the power of MVS, let's consider how Rust's ownership and borrowing system compares to Hylo's MVS model. Rust's ownership and borrowing system is a powerful tool for ensuring memory safety, but it can be complex and may not always provide the benefits that MVS aims to achieve. Consider the following Rust code:
struct T;
fn own_t(t: T) {}
fn ref_mut_t(t: &mut T) {
own_t(*t); // ERROR: cannot move out of `*t` which
// is behind a mutable reference
*t = T;
}
In this example, the ref_mut_t function attempts to move the value t out of the mutable reference, which is not allowed in Rust. This is
because Rust's ownership system does not allow dereferencing a mutable reference to move the value it points
to, as it would violate Rust's guarantees about memory safety. To work around this, you would need to copy
the value or use some other mechanism to transfer ownership, which can introduce overhead and complexity.
In Hylo, the same code would be valid and would not require any special handling, as the language's MVS
model allows for efficient mutation of values without copying.
type T {}
fun own_t(_ t: sink T) {}
fun ref_mut_t(_ t: inout T) {
// In Hylo, we can pass `inout t` as a sink to `own_t`,
// which allows us to transfer ownership without copying.
own_t(t)
// `t` cannot be used after being passed as a
// sink parameter, as it has been moved.
t = T()
}
In this example, the ref_mut_t
function can pass t as a sink to own_t, which allows for efficient mutation of the value without copying.
After own_t is called, t is considered
"moved" and cannot be used until it is re-initialized, which is a safe and efficient way to manage memory.
The Zest's Programming Language
From the Zest's GitHub page: Zest is a (very wip) programming language for building systems that are both malleable and legible. Jamie Brandon, the creator of Zest, writes the Ruminating about mutable value semantics post during his research on the Zest's MVS model. For the purposes of his goal—namely, ensuring that deserialize(serialize(x)) == x—the proposed solutions were not optimal.
The central tension is that every reasonable approach must trade off between:
- Runtime efficiency (avoiding unnecessary copies and overhead)
- Local reasoning (understanding what can mutate what without hidden effects)
- Value equivalence (treating data as purely structural and consistently serializable entities)
In practice, most existing approaches can satisfy at most two of these properties at once:
- Copy-on-write/reference counting: preserves value semantics, but introduces runtime overhead and complexity in performance reasoning.
- Ownership systems: provide strong safety and efficiency guarantees, but significantly restrict expressiveness and increase cognitive load.
- Naive deep-copy semantics: keeps reasoning simple, but quickly becomes impractical for real-world performance requirements.
Beyond these established approaches, Jamie Brandon also sketches a more speculative point in the design space. The idea is to avoid exposing the distinction between owned and borrowed values at the type level entirely. Instead, each access to heap-allocated data would carry an implicit ownership annotation (conceptually an internal “owned vs borrowed” bit), while the compiler decides when sharing or copying is required.
In this model:
- Small values are always copied implicitly,
- Large values may either be copied explicitly or represented via reference counting,
- Borrowed values remain second-class and are never observable to the programmer, and
- Aliasing is strictly controlled and must not leak into observable semantics.
The goal is to preserve a pure value-oriented programming model while still allowing efficient mutation under the hood. This design becomes significantly more subtle once closures and mutation are introduced. Capturing mutable state inside closures reintroduces aliasing concerns: even with copy semantics, hidden duplication of state can lead to surprising divergence between what a closure observes and what is later mutated elsewhere. To address this, the author considers a more constrained model. Closures capture mutable variables by reference rather than by value. Escape analysis ensures closures cannot outlive their captured state. Limited and well-scoped forms of aliasing are permitted under strict rules.
Overall, the exploration reinforces the core theme of the post: every design choice shifts the balance between expressiveness, performance, and reasoning guarantees. Stronger guarantees improve reasoning but reduce flexibility. Higher performance often increases compiler or runtime complexity. Hiding aliasing simplifies serialization but constrains language design. Exposing aliasing improves expressiveness but breaks the pure value model. In conclusion, there is no fully satisfactory solution within the explored space. Ownership-based systems appear too restrictive, reference-counted approaches too costly or unpredictable, and pure copy semantics too inefficient for practical use.
The speculative model presented is therefore best understood as a point in a broader landscape rather than a final design. As the author notes, a more pragmatic path—closer to Swiftlet-style semantics—is likely to be more viable in practice, even if it does not perfectly satisfy all constraints.
1 Consider the Rust programming language, for instance. It features a strong type system and a static analysis—most notably, the borrow checker—that ensures safe code cannot violate memory safety guarantees. However, it is still possible to write code that breaks these guarantees by using unsafe, thereby potentially causing undefined behavior. ↩
2 We refer the reader to the following resources: (i) The research section of the hylo-lang website for a comprehensive list of papers related to MVS, (ii) the Hylo language specification, (iii) the Utilizing value semantics in Swift post, and (iv) the Ruminating about mutable value semantics post. ↩
3 https://hylo-lang.org/docs/user/language-tour/functions-and-methods/ https://hylo-lang.org/docs/user/language-tour/functions-and-methods/ ↩