Programming Language Semantics and Memory Safety |

>archives<br>>artifacts<br>>about

Programming Language Semantics and Memory Safety

2026-08-21

/blog

&emsp;#memory safety

&emsp;#semantics

&emsp;#rust

&emsp;#c

&emsp;#c++

Have you ever wondered what a programming language actually is?

People often say that a programming language is just a tool we use to tell computers what to do. I really don't like this metaphor.<br>Tell me then, how does this tool work?

At university, we may learn that a language is defined by its syntax and its semantics ,<br>along with ways to make these definitions with mathematical precision. For syntax, there is grammar, but for semantics?

Why care?

Memory safety, what else! I have been working on memory safety for a few years now. I helped<br>get Rust adopted at Google as a lead of the Rust team, I joined memory safety standard discussions on behalf of Google. I met professionals with all sorts of view on the topic.<br>I even contributed to design discussions of the Carbon programming language and a bit to its implementation, though unsure whether that matters.<br>I am between jobs at the moment, so for once don't need to worry about the not-my-employer's-opinion disclaimer.

To me, memory safety is a programming language topic. I love PL! It is a wild field of research with conventions and jargon that most people don't have access to. Hopefully this<br>article fixes that a little bit.

Memory safety would actually be an opportunity to put PL research into the spotlight! Alas, there are broad, political reasons that make fact-based discussions hard.

When grown-ups talk about safety, they really mean cybersecurity. Preventing attacks is the main concern and driving force, conventions, testing, mitigations just won't cut it.

security is risk-based and thus a frequent exercise in making trade-offs and economic arguments.

the world is drowning in legacy code

Investing into security involves uncertainty, even if it is clear that something needs to change.<br>We don't need to fully replace C and C++ in order to significantly improve security, but it will cost - time and money.<br>When fighting over limited resources, you will not only find honest people arguing over hard decisions and also people who push a more selfish agenda.

I think academic PL people are a lot like mathematicians in that they practical application of their work, hoping someone with money and influence will discover their work and put it to good use.

So I will do the same! What follows is an invitation to get back to the science of programming. If you want your compiler and libraries<br>to work correctly and be secure, someone has to argue from principles.

Diving into formal semantics

When you write x = y + 1, how do we formally define what that means? It turns out, there are three main ways to look at it: Operational , Denotational , and Axiomatic semantics.

These sound like intimidating academic terms, but as a working developer, you already intuitively understand the concepts. You just know them by different names: interpreters, compilers, and assertions. All these views on languages are simultaneously useful.

To break this down, let’s invent a tiny toy language. It has arithmetic, immutable variables (let), and mutable variables (var).

Here is a snippet of our toy language:

var x = 0;<br>let y = 5 in<br>x = y + 1

x is a mutable variable initialized to 0. y is an immutable variable bound to 5. Finally, we update x.

Let’s look at this snippet through the three lenses of formal semantics.

1. Operational Semantics: The "Interpreter" View

The core question: How do we execute this code step-by-step?

Operational semantics defines a program's meaning by describing how it executes on an abstract machine. It is less concerned with "what it mathematically is" and more concerned with "how it runs."

If you have ever written an interpreter, you have provided an operational semantics. It may not the best choice for typesetting and and publishing it in an article or book, but a program<br>can certainly count as providing rules defined with mathematical precision. The researchers use a set of logical rules (often called Structural Operational Semantics) that involve rewriting<br>a bunch of formal symbol strings. But practically, the essence is this:

We keep track of a State (a mapping of mutable variables to their values) and an Environment (a mapping of immutable let bindings to their values).

Initial State: { x: 0 }, Env: {}

Evaluate let y = 5. We add y to the environment.<br>State: { x: 0 }, Env: { y: 5 }

Evaluate x = y + 1. We look up y in the Env (5), add 1, and update x in the State.<br>State: { x: 6 }, Env: { y: 5 }

Why developers care: Operational semantics is the most common way to define language specifications. We just expect that it is clear and well-defined what happens when a line of code runs. When the ECMAScript specification describes how JavaScript should execute, it uses a form of operational semantics. It answers the...