Free Understanding Computation by Tom Stuart Page B

shown several different ways of approaching the problem of giving computer
     programs a meaning. In each case, we’ve avoided the mathematical details and tried to get a
     flavor of their intent by using Ruby, but formal semantics is usually done with mathematical
     tools.
    Formality
    Our tour of formalsemantics hasn’t been especially formal. We haven’t paid
     any serious attention to mathematical notation, and using Ruby as a
     metalanguage has meant we’ve focused more on different ways of executing
     programs than on ways of understanding them. Proper denotational
     semantics is concerned with getting to the heart of programs’ meanings
     by turning them into well-defined mathematical objects, with none of the
     evasiveness of representing a Simple «
while
» loopwith a Ruby
while
loop.
    Note
    The branch of mathematics called
domain
     theory
was developed specifically to provide definitions
     and objects that are useful for denotational semantics, allowing a
     model of computation based on fixed
     points of monotonic
     functions on partially
     ordered sets . Programs can be understood by “compiling” them
     into mathematical functions, and the techniques of domain theory can
     be used to prove interesting properties of these functions.
    On the other hand, while we only vaguely sketched denotational
     semantics in Ruby, our approach to operational semantics is closer in
     spirit to its formal presentation: our definitions of
#reduce
and
#evaluate
methods are really just Ruby
     translations ofmathematical inference rules.
    Finding Meaning
    An importantapplication of formal semantics is to give an unambiguous specification of the
     meaning of a programming language, rather than relying on more informal approaches like
     natural-language specification documents and “specification by implementation.” A formal
     specification has other uses too, such as proving properties of the language in general and
     of specific programs in particular, proving equivalences between programs in the language,
     and investigating ways of safely transforming programs to make them more efficient without
     changing their behavior.
    For example, since an operational semantics corresponds quite closely to the
     implementation of aninterpreter, computer scientists can treat a suitable interpreter as an
     operational semantics for a language, and then prove its correctness with respect to a
     denotational semantics for that language—this means proving that there is a sensible
     connection between the meanings given by the interpreter and those given by the denotational
     semantics.
    Denotational semantics has the advantage of being more abstract than operational
     semantics, by ignoring the detail of how a program executes and concentrating instead on how
     to convert it into a different representation. For example, this makes it possible to
     compare two programs written in different languages, if a denotational semantics exists to
     translate both languages into some shared representation.
    This degree of abstraction can make denotational semantics seem
     circuitous. If the problem is how to explain the meaning of a
     programming language, how does translating one language into another get
     us any closer to a solution? A denotation is only as good as its
     meaning; in particular, a denotational semantics only gets us closer to
     being able to actually execute a program if the denotation language has
     some operational meaning, a semantics of its own
     that shows how it may be executed instead of how to translate it into
     yet another language.
    Formal denotational semantics uses abstract mathematical objects, usually functions, to
     denote programming language constructs like expressions and statements, and because
     mathematical convention dictates how to do things like evaluate functions, this gives a
     direct way of thinking about the denotation in an operational sense. We’ve taken the less
     formal approach of thinking of a