thread safety

Stable, Mutable References

By Jake Fecher in mutability, thread safety, memory management

2025-08-21

This post is an exploration on some additional possible semantics for mutability (and immutability). Introduction In my first blog post I introduced &shared mut references as a way to achieve safe, shared mutability in a language with unboxed types. For those unfamiliar with them, I encourage you to start with the first blog post. As a brief summary though, I started with Rust’s system with owned mutable references which I referred to as &own mut, and added on &shared mut from there.

Continue reading

Algebraic Effects, Ownership, and Borrowing

By Jake Fecher in effects, thread safety, memory management

2024-02-20

Introduction Algebraic Effects are a useful abstraction for reasoning about effectful programs by letting us leave the interpretation of these effects to callers. However, most existing literature discusses these in the context of a pure functional language with pervasive sharing of values. What restrictions would we need to introduce algebraic effects into a language with ownership and borrowing - particularly Ante?1 Ownership Consider the following program: effect Read a with read : Unit -> a the_value (value: a) (f: Unit -> b can Read a) : b = handle f () | read () -> resume value This seems like it’d pass type checking at first glance, but we can easily construct a program that tries to use the same moved value twice:

Continue reading

Achieving Safe, Aliasable Mutability with Unboxed Types

By Jake Fecher in mutability, thread safety, memory management

2024-01-29

This is part of Ante’s goal to loosen restrictions on low-level programming while remaining fast, memory-safe, and thread-safe. Background When writing low-level, memory-safe, and thread-safe programs, a nice feature that lets us achieve all of these is an ownership model. Ownership models have been used by quite a few languages, but the language which popularized them was Rust. In Rust, the compiler will check our code to ensure we have no dangling references and cannot access already-freed memory (among other errors).

Continue reading

Contents