What is Semantics?

A formal semantics of a programming language is a precise, rigorous, and unambiguous mathematical definition of the behaviors of all programs in that language. This means that every possible action a program can take—every state change, computation, or output—is fully and completely described in terms of mathematical axioms, leaving no room for misinterpretation or ambiguity.

When studying a language—whether it's a natural language like English or a programming language like JavaScript—you focus on two key aspects:

• Syntax: The structure of the language (rules for how to write it)

• Semantics: The meaning of the language (what the written symbols mean)

You’ve actually encountered these concepts before, just under different names. In grade school, you learned syntax as grammar and semantics as reading.

In programming, syntax defines what constitutes a well-formed program, while semantics describes what that program does when executed. As John Reynolds famously put it,

Semanticists should be obstetricians, not coroners of programming languages

This means semantics should give birth to better languages from the outset, not merely dissect them after the fact.

Why does this matter to us?

At Pi Squared, we develop technologies and solutions for all programming languages, via a formal semantics framework called the K framework.

To achieve this, we need to understand two things about a programming language:

• What is a well-formed program? → This is syntax

• What does a well-formed program do? → This is semantics

Our ambition goes beyond merely executing programs. We aim to define their behavior in a mathematically rigorous and unambiguous way, ensuring consistency and correctness across all languages. This is where formal semantics becomes indispensable.

The ideal scenario, as envisioned by modern language design pioneers, is to define a language’s syntax and semantics once and have all necessary tools automatically generated from that definition, correct-by-construction and backed by rigorous, machine-checkable proofs.

At Pi Squared, we’re not just dreaming of this future—we’re building it with the K framework, leveraging semantics to create a verifiable, trustworthy execution environment free from the technical debt of ad-hoc implementations of interpreters, compilers, or transpilers

So, basically, we adopt a semantics-based and semantics-first approach to offer correct-by-construction tools for all languages.

Why any language?

Even though languages are different, oftentimes, they are able to express the same ideas. So, why do we need the K framework? Aren’t all languages essentially the same?

The short answer: Not exactly.

The reality is that it’s sometimes easier to say a thing in one language, than in the other. For instance, let’s say you have two sentences in different languages, but with the same meaning:

• “It's raining heavily outside” (English) - 8 syllables

• “下大雨" (Xià dàyǔ)” (Chinese) - 3 syllables

Now, programming languages work similarly—but with one key difference. While human language semantics are typically static (a word or sentence describes a fixed snapshot in time), programming language semantics describe dynamic processes (a program executes and changes state over time).

• Human language semantics: "The cat is on the mat." (Describes a state)

• Programming language semantics: x = x + 1 (Describes a process)

When this statement x = x + 1 is executed, the current value stored in the variable x is retrieved, 1 is added to it, and the result is then stored back into x, updating its value.

It's important to recognize that while we often use human language to explain what a piece of code does (as we did above for x = x + 1), this is still a description.

Entire books, sometimes thousands of pages long, are written in English (or other natural languages) to describe the syntax and semantics of a programming language. These are called the “specifications” of a language.

The crucial difference with the K framework is that it moves beyond these natural language descriptions. Instead of relying on potentially ambiguous human language, K uses a formal, mathematical approach to define the semantics of a programming language.

This means that the behavior of every construct, like the assignment x = x + 1, is defined through mathematical axioms and rules, leaving no room for ambiguity.