The Story of Denotational Semantics

My Cliff Notes for the story of denotational semantics:

1. We want to model programming language elements with their natural analogs in mathematical sets: numbers as numbers, functions as functions, etc.
2. We want recursive functions in our language. But recursive definitions aren't really definitions, but rather constraint specifications. For example, × should be the least function such that 0 × n = 0 and (m + 1) × n = n + (m × n).
3. So we want a fixpoint operator fix that takes a constructor function f, which tells us how to build successive approximations of the recursive function, and gives us the actual recursive function.
4. The constructor function tells us how to improve an approximation of the solution to the constraint. Thus, the actual solution, which should be the limit of the sequence of approximations, should be a fixed point of the constructor: applying the solution to f should result in the same solution. Hence the specification of the fixpoint operator fix f = f (fix f).
5. The fixpoint operator should have the property that it will always give us a unique solution for any reasonable recursive function definition.
6. It so happens that if we restrict our model to allow only continuous functions, this fixpoint operator exists. The continuous functions are functions where these sequences of approximations exist, i.e., the limit of the sequence behaves consistently with each of the approximations. This is natural: in order for the partial results to be approximations of the real thing, we expect them to be getting closer to the result.
7. So because the existence of the fixpoint operator depends on our functions being continuous, we always have a proof obligation that any constructor in the denotational semantics that produces a function in fact produces a continuous function.

Sam pointed out that all this shows the importance of Turing's proof of the undecidability of the halting problem: all of these problems arise when we have to worry about the behavior of functions at infinity. If we could simply disallow ⊥ from the language, and static analysis could always prove a function to be terminating, then we wouldn't have to deal with any of this.