You could have invented denotational semantics!
Suppose you want to know if some property about a program or a programming language holds. For example, you might wish to know whether a static analysis you’ve come up with provides a runtime guarantee. You could just write some tests to verify it empirically, but you can’t exhaustively test all possible cases, so this isn’t enough to say for certain there aren’t corner cases where it fails.
The only way to be completely certain is to prove your property, and this necessarily means you are entering the realm of mathematical reasoning. Proofs can be done to varying degrees of formality, but even an informal proof requires some structured plan of attack. Broadly speaking, there are two routes you might take:
You could choose to phrase your property entirely syntactically. You can define the syntax of your language and define syntactic rules (like typechecking judgments and reduction rules) for analyzing and transforming its terms. Then you can perform proofs about what invariants these syntactic manipulations preserve.
One example of this technique is proving type soundness via progress and preservation. You can prove that it’s always possible to reduce a well-typed term until it reaches some value (progress) and that this reduction doesn’t change the expression’s type (preservation). These are mathematical statements about the language’s symbol-manipulation rules, but they refrain from assigning any particular meaning to the symbols. They just prove properties about what the typechecker and evaluator happen to do.
This syntactic approach is known as operational semantics because the analysis is performed on a model of the language’s actual operational mechanisms: typechecking judgments correspond to a typechecker, and reduction rules correspond to an evaluator.
A second approach would be to phrase your property semantically. You could say that numbers in your programming language mean (correspond to) mathematical numbers, and a lambda term means a mathematical function. That is, for each term in your language, you can map its syntax onto some mathematical concept that reflects its structure.
An immediate advantage of doing this is that we already know lots of properties about mathematical structures. If your mapping from syntactic terms to mathematical objects is an adequate model for your language—that is, equivalences in your denotational model imply equivalences in an operational model and vice versa—you can now reason about your programs entirely in terms of the realm of mathematical objects! This lets you get away from worrying about nitty-gritty syntactic details that are otherwise uninteresting bookkeeping.
For example, in purely a syntactic approach, (x + y) + z is a different term from x + (y + z), and you cannot simply treat them as interchangeable. However, if numbers in your language really do work just like mathematical numbers, then you can work in the language of mathematics, and the distinction ceases to exist.
Since this approach chooses to interpret the syntactic terms of the programming language by giving them some mathematical meaning, or denotation, we call this approach denotational semantics.
One way to think about denotational semantics is that it does some work up front to translate terms of a programming language into a domain-specific language for doing reasoning: mathematics. In this sense, it’s not entirely unlike the way a compiler desugars a source language into a simpler IR that is easier to work with. However, instead of simply mapping terms into a smaller, simpler grammar, we’re mapping them into a mathematical domain.
A brief illustration
Suppose we want to provide a denotational semantics for the following extremely simple arithmetic language:
$$\begin{array}{rcl}
\mathit{expr} \hskip{-10mu}&::=&\hskip{-10mu} \mathsf{zero}\\
&|&\hskip{-10mu} \mathsf{succ}(\mathit{expr})\\
&|&\hskip{-10mu} \mathsf{add}(\mathit{expr}, \mathit{expr})\\
&|&\hskip{-10mu} \mathsf{mul}(\mathit{expr}, \mathit{expr})
\end{array}
$$
(Here, $\mathsf{succ}$ is the successor function.)
First, we need to pick a mathematical domain to map these syntactic terms into. Since this language represents arithmetic on natural numbers, we’ll choose ℕ, the set of natural numbers, as our mathematical domain.
Next, we need to actually define the mapping from syntactic terms to our domain. To do this, we traditionally use the notation $⟦x⟧$ to mean “the denotation of $x$”. (The $⟦\,⟧$ brackets themselves are usually called “double square brackets” or “white brackets”.) For our language, we could therefore define our semantics this way:
$$\begin{aligned}
⟦\,\mathsf{zero}\,⟧ &:= 0 \\
⟦\,\mathsf{succ}(x)\,⟧ &:= ⟦\,x\,⟧ + 1 \\
⟦\,\mathsf{add}(x,y)\,⟧ &:= ⟦\,x\,⟧ + ⟦\,y\,⟧ \\
⟦\,\mathsf{mul}(x,y)\,⟧ &:= ⟦\,x\,⟧ × ⟦\,y\,⟧
\end{aligned}
$$
Assuming this is, in fact, an adequate model for our language, we can now prove things about programs by taking advantage of facts we already know about mathematics. For example, we can prove that
$$
\mathsf{add}(x,y) ≡ \mathsf{add}(y,x)
$$
via the argument
$$\begin{aligned}
⟦\,\mathsf{add}(x,y)\,⟧ &= ⟦\,x\,⟧ + ⟦\,y\,⟧\\
&= ⟦\,y\,⟧ + ⟦\,x\,⟧ \\ &= ⟦\,\mathsf{add}(y,x)\,⟧
\end{aligned}$$
which uses the commutativity of addition on natural numbers. If we were to prove the same property using operational semantics, we’d need to make an inductive argument about the language’s evaluator, which would be significantly more involved!
Denotational semantics of real programming languages is, of course, significantly more involved, but a full discussion is well outside the scope of this answer. However, the essential process is the same: select a domain, map each of the terms of your language onto that domain, and then write proofs that take advantage of the structure of the domain.
The choice of domain
For many languages, the interpretation of its terms may seem “obvious”. For example, it might seem like numbers in the programming language “ought” to be mapped onto mathematical numbers, and functions “ought” to be mapped onto mathematical functions. However, in practice, this is often not the most useful approach, for a few reasons:
Programming language concepts often do not correspond precisely to the mathematical concepts we informally think of them as. For example, mathematical natural numbers satisfy the following property:
$$
\forall\, n ∈ ℕ.\: n + 1 > 0
$$
However, fixed-size unsigned integers in programming languages do not! Therefore, natural numbers are not a semantically valid interpretation for fixed-size unsigned integers. Instead, the more complicated domain of integers modulo $2^n$ must be used.
Some expressions in a programming language might not correspond to any value in the mathematical sense, such as exit(-1). In these cases, it may be useful to map expressions of this sort onto some token value in the target domain, often notated as $⊥$ or $↯$.
Imperative features like mutable state require some additional structure to model mathematically. There are often many different ways to represent that structure, and which one is the most useful may depend on what properties you’re trying to prove.
Capturing recursive functions or other potentially-unbounded structures can be mathematically challenging, so much so that we have an entirely separate question dedicated to it: How can we define a denotational semantics for recursive functions?
In some cases, there may be structure in your language you explicitly don’t want to preserve. For example, there may be expressions that are distinguishable within your language, but they are interchangeable from the perspective of the property you’re trying to prove. Therefore, you may choose to map several different values in your source language onto the same object in your mathematical domain, which is a form of abstract interpretation.
Sometimes, finding the most useful domain to interpret your syntax in is actually the hardest part of proving something using denotational semantics! Indeed, this reflects the idea that denotational semantics is about “getting into the right language” to be able to prove something.
