Programming Language Foundations

Theory of Programming Languages

---

Introduction

Classically, the study of programming languages is split into syntax and semantics, where syntax refers to the grammar and the syntactic rules of the language, whereas semantics refers to the meaning and validity of sentences in the language. However, modern theory has moved on from studying the formal structure into something more abstract where programs are considered to be mathematical objects governed by statics and dynamics.

• Statics define features of the programming language, such as how terms and programs are formed and how the terms are typed.
• The dynamics define how these features behave at “runtime”, i.e. during evaluation or execution. The dynamics can rely on the invariants placed by the statics, such as “variable x is an integer”, to provide safe (and usually deterministic) behavior for the programs.

We still talk about the different roles of syntax and semantics, as they are key notions in logic. Logics are in many ways similar to programming languages. Syntactic notions that are common between the two include variables, functions, substitution and quantifiers. However, deeper correspondences are also found in their semantics, as shown in the following table describing the famous Curry-Howard correspondence (also known as the “propositions as types” interpretation).

Logic	Programming languages	How they correspond?
Formula	Type	Formulas are like the type of “all possible proofs” of that formula
Formula is true	Inhabited type	A formula is true if its corresponding type has at least one element
Formula is false	Uninhabited type	A formula is false if its corresponding type has no elements
Proof	Term	A proof of a formula is a term that witnesses that its type is inhabited
Conjuction	Pair/product type	Both tie together two pieces of information from which both constituents can be extracted
True (logical constant)	Unit type	True has a trivial proof and the unit type has a trivial element
False (logical constant)	Empty type	False cannot be proven without inconsistent assumptions, and an element of an empty type cannot be constructed1 without inconsistent arguments
Disjunction	Sum type	Both tie together either one of two pieces of information. To extract information, one has to analyze both the left and right cases.
Implication	Function type	An implication between formulas and corresponds to a function that transforms any proof term of to
Modus ponens	Function application	Using an implication to to get corresponds to applying a function to a proof term of to get a proof of

Notice how these are all features of the statics of programming languages — the correspondence between logic and programming languages is in the type system. The dynamics are pretty much irrelevant from a logic perspective as the primary function of dynamics is to compute a result from a well-defined computation — to make the computer do stuff.

The process of building the calculator in the previous chapter consisted of roughly these three steps:

1. Parsing source text to CST.
2. Converting the CST to an AST.
3. Calculating the value of the computation encoded in the AST.

Parsing, type checking and converting from CST to AST are part of the statics of the language, whereas doing the computation is part of its dynamics. In a later chapter we will add a type checker which sits somewhere between 1 and 3.

Loading Exercise...

For a more thorough look at programming language theory, have a look at the following textbooks

• Types and Programming Languages by Benjamin C. Pierce.

  A thorough and approachable book that covers almost all currently relevant programming language properties. This book was the primary inspiration for this whole course.

• Practical Foundations for Programming Languages by Robert Harper.

  A bit more logically thorough approach to programming languages than Types and Programming Languages.

• Essentials of Programming Languages by Friedman and Wand (free).

  A very concrete approach to designing programming languages. The book uses scheme, a member of the LISP programming language family, for all of the implementatino code.

• Introduction to the Theory of Programming Languages by Bertrand Meyer (free).

  Covers all the basics very thoroughly and uses a common knowledge concepts for examples.

• Programming Language Foundations (free).

  A one hundred percent formalized and machine-checked book about developing the simply typed lambda calculus from scratch using a proof assistant.

The most approachable textbook is Types and Programming Languages (in the author’s opinion) after which the next logical step is Practical Foundations for Programming Languages

All of these resources are recommended supplementary reading, but understanding the theory of programming languages thoroughly is not required on this course.

Motivation: Type Safety

Designing a programming language involves various considerations. Many of them are related to the syntax of the language, but more importantly, designing a language whose semantics adhere to a consistent logic can be challenging without knowing some key properties to aim for. These key properties, which we will focus on in a later part of the course are as follows:

• Preservation: a typed programming language (with well-defined evaluation⁵) “preserves types”, if the a term can only evaluate to other terms of the same type.
• Progress: every term that is not already a value can evaluate to another term, i.e. terms never get “stuck”.

Together these properties are called type safety or type soundness.

Unsafe in Rust

As described in the articles above, Rust has a special keyword for unsafe where some of Rules of safe Rust don’t aren’t enforced. It is a common misconception that within an unsafe block, one is able to write C-style code without worrying about the borrow checker and other Rust-related headaches. This, however, is not the case at all and the so called unsafe superpowers are much more limited than this.

Notice how, for example, unsafe does nothing to disable the borrow checker, the enforcer of Rust’s ownership rules.

Another common misconception is that unsafe code is somehow incorrect or unsafe to use. This is obviously not the case since the Rust standard library contains loads of unsafe code. What is the exact purpose of unsafe then? Well — unsafe code is mainly used in places that rely on invariants that cannot be encoded or enforced by the type system. Another common occurrence of unsafe is whenever calling non-Rust (usually C) code from Rust. Unsafe is needed simply due to the fact that Rust cannot guarantee that the non-Rust code follows Rusts safety rules.

Writing correct unsafe code is way out of the scope of this course and is something even experienced Rust developers struggle with. Unsafe isn’t meant to be ergonomic to write and the lack of ergonomics is there to also force the author to think about all the possible things that could go wrong with their code. It is for example customary (and usually also enforced) to leave a // Safety: comment next to every unsafe block that gives a detailed explanation of the invariants and why they always hold so that the code is safe. Writing this comment forces the developer to defend the correctness of their code and inconsistencies are surprisingly often found while writing the comment.

Before writing a single line of unsafe it is recommended to read the Rustnomicon. For a good overview on unsafe, check out The Rust Programming Language or Chapter 9 from Rust for Rustaceans.

Reading Exercise

Next, please read the following articles, and after reading them answer the quizzes below.

• How Safe and Unsafe Interact is the introduction to Rust’s unsafe feature. If you don’t know what undefined behavior is, you should glance over this Wikipedia page. Also have a look at what the Ord trait and BTreeMap are in Rust.
• What Type Soundness Theorem Do You Really Want to Prove? explains what type safety is and how it’s limited in the presence of unsafe Rust. If you want to watch a video as well, this recording of a keynote by Derek Dreyer covers many of the same things but also much more.

For even more reading, see chapter 6 in Practical Foundations for Programming Languages.

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Loading Exercise...

Miri

Miri is an extremely interesting Rust development tool used to detect undefined behavior. It works by interpreting the mid-level intermediate representation (MIR) of Rust and checking for undefined behavior and memory leaks. Miri is an excellent tool that has discovered many real-world bugs

It is important to note that Miri isn’t able to prove that a program is sound since it only explores concrete executions. However, Miri can definitely prove that a program is unsound by finding undefined behavior while evaluating it.

If you’re interested to learn how Miri works, we recommend reading this paper describing Miri.

Inference Rules

Inference rules, are a construction from logic which allows us to clearly express a (commonly recursively defined) language (or a relation). Inference rules consist of a set of premises and a conclusion, and when written down, the premises and conclusion are visually separated by a horizontal line. The premises and conclusion are judgments which can be thought of as “true statements”.

For example, given two logical formulas and , one typically calls ” is true” or just "" a judgment of logic. Now, in natural deduction, we add rules or transformations between judgments to create a way to combine them and break them apart. For example, a rule of inference in natural deduction called modus ponens states that if implies and then we get . This inference rule is written as follows:

In logic, judgments are purely syntactic, i.e. don’t require any meaning to be attached. If the premises and are true, then is true, not because implication carries any meaning, but instead because the rule says so. When we take something as granted in mathematics, we typically call that an axiom. Inference rules are more than just axioms⁶, they can be used to infer somethings starting from the axioms, or by combinding previous results.

To demonstrate the syntactic nature of judgments, let’s run through a simple example. We will work in a language of relations between natural numbers where the relation is denoted with the symbol. None of the symbols (or numbers) have any meaning — they are merely abstract syntax.

Now, suppose we take as axioms that and for any if then . We also have one inference rule: the modus ponens shown earlier. With the inference rule we can deduce with the following deduction (also known as a proof tree or a derivation tree)

The deduction is valid because is the first axiom, and is a special case of the second axiom.

We also refer to a judgment as valid, if there exists a deduction which only uses the given inference rules and axioms.

Loading Exercise...

Peano Arithmetic

Peano arithmetic is an axiomatization of the natural numbers and their operations. We will shortly prove that from the Peano axioms as an exercise in mind numbing formal logic :D

First, the formal language that we will use is first-order logic. If you are unfamiliar with first-order logic, it’s syntax consists of terms, sentences, equalities, propositional connectives and quantifiers.

As a reminder, propositional connectives are , and quantifiers are (for all) and (exists).

By default, only variable names are terms in first-order logic, but we also have the constant symbol and function symbols and in the language as we are working with Peano arithmetic. The role of is the “successor” of a natural number. There’s no need to give it any meaning, except perhaps for intuition: successor of means .

If you are not sure what all this means, don’t worry, it should all make more sense soon.

Examples of terms in the language are

Terms shouldn’t be confused with sentences, so we give a few examples of sentences in the language:

The last sentence is the encoding of the statement using zero and the successor function . It needs to be encoded this way because is nonsense in the language we are working in.

Next, let’s explore the axioms — the sentences from which all other results (like ) are deduced. The following axioms are from the first-order theory of Peano arithmetic. We will only look at the first four, although there are seven in total⁷.

The first two axioms guarantee that the successor function takes a number to a new number without creating cycles. The last two axioms characterize how addition should behave, and are the key axioms we will use in our proof of .

To finally prove our main result, i.e. deduce it from the axioms, we need the inference rules of first-order logic. As there are quite a few of them (and vary somewhat depending on the source), we will only list ones that we use.

Modus ponens, is one of them, and is denoted (“e” stands for “elimination”).

• Let be formulas. From and we can deduce :

Notice how the name of the inference rule is written on the right side of the inference line.

The elimination rule of universal quantification says that you can deduce something from a universally quantified formula. It’s a bit tricky because it involves a substitution which has to be valid⁸. Luckily, in our proof we won’t run into any substitution problems.

• Let be a formula, be a term and a variable. From we can deduce where is substituted for ():

We also need axioms about equality. The following axiom states that equality is transitive, i.e. from and we get :

Notice that the curried style is equivalent to , i.e. the axiom has “two hypotheses”.

An the following states that equality is congruent with the function symbols ( in this case):

can now be deduced from the axioms using these rules.

The high level proof structure goes like this: We prove and , and using the transitivity of equality, get ().

The colors are only used to visually track the roles of the different formulas.

To fill in the actual inference rules, we begin by proving .

The deduction is valid because all inferences end up at an instance of an axiom. Now in the main proof, we can refer to the above deduction by the name where denotes the proof tree and its conclusion.

The deduction is valid because all inferences end up at an instance of an axiom. The axioms used were:

• (Peano axiom 3)
• (Peano axiom 4)
• (Congruence of equality)
• (Transitivity of equality)

Loading Exercise...

Formation Rules

Now that we have explored how axioms and inference rules can be used to express Peano arithmetic, we will move to a more programming language related topic: formation rules and trees. Also, now that we are not working with logic and natural deduction, we call our inferences derivations (or derivation trees) instead of deductions.

The set of propositional formulas is defined as follows:

This definition captures the syntax of propositional formulas, but says nothing about their semantics, i.e. meaning. To avoid confusion when talking about formulas like we use explicit parentheses, as in the definition. Operator precedence rules could be also used to implicitly add parentheses. For example has a higher precedence than which is higher than which is higher than , so is parenthesized .

Formation rules, like BNF, are a convenient way to write down the rules of a grammar. Instead of defining a concrete grammar with whitespaces and whatnot, formation rules define a more abstract syntax which closely resembles an AST.

We can express the formation rules of propositional formulas using inference rules. A judgment in this case would be that ” is a well-formed propositional formula” and is shortened to just ” wff”. A formula is said to be well-formed if it can be constructed from the formation rules in a finite number of steps.

The formation rule for negation says that if is a well-formed propositional formula, then is a well-formed propositional formula. In inference rule format, this is expressed as follows:

The subscript “f” stands for “formation”.

And the formation rule for conjunction has two premises: and need to be well-formed.

As an example, let’s derive that is a well-formed propositional formula.

How do we show that is well-formed? Well, as is a lowercase letter, it’s a propositional variable. Obviously variables are well-formed, so we need a an axiom for those. A rule might work as well, but we need one for each of the variables which would mean we need an infinite amount of rules. So let’s add an axiom for every variable :

The completed derivation (or formation tree) of the well-formedness of is:

The derivation is valid because each inference ends up in an instance of the propositional variable axiom.

Formation Rules of Prefix Arithmetic

The arithmetic language defined in the previous chapter can also be expressed in terms of formation rules. The judgments have the shape "" where is just a name for the set of well-formed terms of prefix arithmetic.

Non-negative integer literals are the only atomic terms of the language, so we take as an axiom for all . The other rules are for the three arithmetic operators.

If and are well-formed terms, then by the above rules we get that , and are also well-formed terms (of prefix arithmetic).

As an aside: in the formation rules, we ignore whitespaces and allow parentheses to be added ad-hoc.

As an example, here’s the formation tree of :

Loading Exercise...

Loading Exercise...

Footnotes

Footnotes

1. Notice that in programming languages like where functions don’t need to be total, it’s trivial to define a term of any type (including the empty type) as we can use infinite recursion (or panics) to get any type :

   problem : T
   problem = problem

   ↩

2. Idris, a language for type driven development, type safe zero-cost abstractions in Rust ↩ ↩²

3. Rust users forum Haskell Wiki ↩ ↩²

4. Annals of Formalized Mathematics, a journal that publishes articles about formalized mathematics and mathematical applications of proof assistants. ↩

5. Many statically typed languages have a compiler without a formal specification for how terms evaluate. What happens to terms and values at runtime is irrelevant for the language to “preserve types”, because type checking always happens at compile-time. Compilers can however assume that preservation holds in order to do optimizations like code inlining correctly. ↩

6. See this mathematics StackExchange post for more information. ↩

7. Plus the standard axioms for equality. ↩

8. A substitution is valid when no free variables in the substitute gets captured in the formula. This is something we need to also worry about when defining the semantics of lambda calculus. ↩