Maxim Zaks mzaks

Refinement types in Scala and contracts in Mojo: a comparison

Oct 13, 2026 · @Maxim

The paper "First-Class Refinement Types for Scala" and the contract verifier being built for Mojo solve overlapping problems from opposite ends. The paper puts facts on types and keeps the solver small; the Mojo work puts facts on functions and uses an SMT solver. They are complementary: the paper's approach suits facts about one value, ours suits relations across a call and code that mutates memory.

The two approaches in brief

The paper (Bovel, Kunčak and Odersky, EPFL) adds refinement types to Scala 3. A refinement type is a type with a predicate, so the fact travels with the value:

JWT-shaped tokens, in a binary format

Or: one thing you can build with Dagr's customizable header — a signed, verify-before-parse binary token.

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. You don't need the others to follow along; this one is about attaching a signed, self-describing envelope to a buffer.

What a JWT actually is

There are two ways an authority can trust who you are. Picture two everyday scenarios.

We swapped Zed's storage layer for Dagr

Or: what happens to an AI agent's chat history when you stop treating it like a JSON blob.

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. In Let's talk about structured logging I promised case studies of DataSink cutting size and improving performance in real applications. This is the first one, and it is a big one: Zed, a production code editor written in Rust.

Why Zed, and why agent history

Most of this series demonstrates Dagr on toy schemas. That is fine for explaining a wire format, but it never answers the question people actually ask: *does this hold up inside a real application that someone else

The Dagr series

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more.

This is the running index for the series. Each post stands on its own — read them in any order — and every one links back here so you can find the rest. I'll keep this list up to date as new posts land.

Posts

Dagr and the five Why Nots — why Dagr exists, and the five conventional choices it deliberately doesn't make.
WTF is per-node layout polymorphism? — combining the best of Protocol Buffers and FlatBuffers by picking a wire layout per node.

Let's talk about structured logging

Or: why JSON is terrible, JSONL is good but not great, and what Dagr's DataSink does instead.

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. You don't need the others to follow along; this one is about append-only streaming of structured data.

What's wrong with JSON?

JSON has become the hammer everyone reaches for when it comes to storing or representing data. And why shouldn't it be — the industry has spent tons of time and resources making JSON serde extremely convenient.

Untapped potential of fixed-size buffers

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. You don't need the others to follow along; this one is about a container called SharedBuffer, for fixed-size, zero-copy buffers.

Look Maaa, serde without serde

Back in June I showed Dagr to my friend Ivan Najman — walked him through everything you can do with a data graph: use it as a replacement for SQLite for your application data, lazy-load large configurations, build small network messages, yada yada yada. He looked at all of it and asked me: can I use Dagr as an interop layer between a WASM worker and a TS renderer?

He is building an interactive simulation, which he documents on his devlog. The simulation

WTF is per-node layout polymorphism?

Or: how to combine the best of Protocol Buffers and FlatBuffers in one format — and take one dependency out of your project.

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. You don't need the others to follow along; this one is about choosing a different wire layout per node.

The world: two formats, two philosophies

Protocol Buffers and FlatBuffers are two different binary serialization formats with two different goals.

Required fields, minus the regret

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This is part of a series on what it can do — the series index lists every post. You don't need the others to follow along; this one is about safely deprecating required fields.

Required fields have a bad reputation — and mostly it is deserved. But I think we can rehabilitate them.

If you have worked with Protocol Buffers or FlatBuffers, you probably know that required fields are frowned upon, because they get in the way of evolving your schema.

While developing Dagr, I keep searching for the inherent complexity of serialization: what actually motivates a given design decision, and what possibilities open up once you take it seriously. So let's start from first principles.

Dagr and the five Why Nots

Dagr is a schema-driven binary serialization format: you describe your data once and it generates zero-dependency reader/writer libraries in Swift, Rust, TypeScript, and more. This post opens a series on what it can do and why it exists — the series index lists every post, and later ones go deeper on specific features.

Why not text based?

For over 10 years I have been making my case that text based data serialization formats are very inefficient and have only one benefit: debug-ability. This is why Dagr is a binary data serialization format, but with a very big focus on developer experience. The Dagr CLI has an option to generate random fuzz examples for a provided graph. Users can generate a browser for the binary file with search and filter functionality and even edit capabilities. The file browser is a self-sustained HTML file with zero dependencies, where you can just drop in the binary file and start bro

	from benchmark import benchmark, Unit, keep, Bencher, Bench, BenchConfig, BenchId
	from hyperloglog import HyperLogLog


	fn hash_int(x: Int) -> Int:
	"""Simple hash function for integers."""
	var h = x
	h = ((h >> 16) ^ h) * 0x45D9F3B
	h = ((h >> 16) ^ h) * 0x45D9F3B
	h = (h >> 16) ^ h