Introduction

About these notes:

• They are meant as a supplement, not a replacement, for the assigned readings.

• IANA programming language researcher, so the viewpoint expressed here is that of an (interested) outsider.

• They are strongly influenced by Cornell’s CS 4110 and related courses at other universities. I’ve tried to cite sources where appropriate, but let this be a blanket citation for any places that I missed.

What is semantics?

You learned how to use a variety of programming languages in your introductory programming classes and Programming Paradigms. And some of you learned, or plan to learn, how to implement a programming language in Compilers and Language Design.

Using and implementing programming languages might seem to be everything you need to know about programming languages, inside and out, but there’s still something missing. What happens if you write a program, like

#include <map>
#include <iostream>
#include <string>
using namespace std;

int main() {
  map<string,int> m;
  m["foo"] = m.size();
  m["bar"] = m.size();
  m["baz"] = m.size();
  cout << m["foo"] << m["bar"] << m["baz"];
  return 0;
}

…and it doesn’t do what you think it should do? (This actually happened to me.) Is the bug in your code, or in the compiler? This is a question about semantics, which defines the correct behavior of programs.

Since you need to understand a programming language before tackling its semantics, we’ll do some programming in Scheme and ML. And since implementing a language is an excellent way to nail down your understanding of its semantics, we’ll also write an interpreter for a simple ML-like language. But our main focus in this course is on semantics.

Formal and informal semantics

How do we resolve a puzzle like the above?

• Some languages are defined by the behavior of the compiler (or interpreter). Then if the programmer disagrees with the compiler, the bug must be in the program, because the compiler is correct by definition. But what happens if different compilers have different behaviors?

• Some languages have an official definition, like C or C++ written in (legalistic) English or some other natural language. But such definitions can be long, unclear, or even underspecified.

We’d like a way to define semantics that is able to resolve questions like the above, with certainty. More than that, we’d like it to enable automated reasoning about programs, like optimizing code while guaranteeing that its behavior is preserved, or guaranteeing that certain runtime errors can never occur.

The idea behind formal semantics is that the best way for humans and computers alike to reason correctly about programs is using the methods of mathematics and logic.

Programming languages and logics

Those of you who have taken Theory of Computing recall that one example of a “programming language” that has a rigorous formal definition is (encodings of) Turing machines. This makes them suitable for proving some important results, but you know from experience that Turing machines aren’t the most convenient way to program.

On the other hand, real programming languages have been developed to suit the needs of real programmers and the capabilities of real computers, and very few of them have been fully given a formal semantics: Scheme and Standard ML are the ones I know of.

The goal (as I understand it) is to get the best of both worlds. The complexity and diversity of real programming languages leads us to grow formal semantics to cover more and more of their features. But the influence goes in the other direction as well: thinking about formal semantics may lead us to realize that certain features of a language are ill-defined or just plain wrong – or sometimes, it leads to completely new ways of programming.