Denotational semantics

Denotational semantics is an approach to formalizing the meaning of programming languages by constructing mathematical objects — typically elements of a domain — that represent what programs denote. Pioneered by Christopher Strachey and Dana Scott at Oxford in the 1970s, it maps each syntactic construct to a semantic function, and the meaning of a program is the composition of these functions.

The power of denotational semantics is its separation of meaning from mechanism: a program denotes a mathematical object that exists independently of any execution machine. The limitation is that not all computational phenomena — concurrency, probability, mutable state — fit naturally into the original framework. Each extension requires new classes of domains, and the field risks becoming a taxonomy rather than a unified theory.

Denotational semantics proves what programs mean; it does not necessarily capture how humans understand them. The gap between formal denotation and intuitive meaning remains open.