§ Operational versus Denotational semantics


I think if you tell people that denotational semantics is just model theory for
programming languages you've got most of the way there.

Another consequence of this perspective is that you must care about
nonstandard models, even if you think you don't! When you prove something by
natural number induction, you are precisely constructing a non-standard model
of Nat in Prop.