Programming languages are notations to express notions of computation. The von Neumann architecture, for example, through the fetch-decode-execute loop in its Central Processing Unit, induces a notion of computation that is state-based, in that a computation is carried out as a series of state changes, each of which is achieved by one iterand of the fetch-decode-execute loop. This imperative notion of computation gives rise to imperative programming languages, where each program specifies a particular series of state changes. In contrast, a logical notion of computation is stateless: a program is a collection of inference rules, and a computation is carried out to determine whether a query holds, and if it does, under which conditions. For example, given type-inference rules, one may wish to infer the type of a given expression, or to check whether a given expression has a given type, or to determine whether a given piece of concrete syntax, typically a string, is syntactically correct with respect to a given grammar (a.k.a. parsing). And likewise, a functional notion is stateless in that no state is involved to specify the factorial function or the fibonacci function and to compute factorial numbers and Fibonacci numbers, given their index.
Most programming languages are said to be Turing-complete in that we can specify any computation in them. And so none is more expressive than another in that we can simulate one using another (by implementing an interpreter) and we can translate programs from one to another (by implementing a compiler).
Whereas natural languages are described using grammars and these grammars evolve to continue to account for the evolving practice of these languages, programming languages are prescribed by their grammar. If a putative program is not grammatically correct, it is not a program.
Data—the representation of information—is often partitioned depending on the type of information we want to represent: integers, booleans, characters, strings, pairs, functions, arrays, etc. Trying to add apples and oranges while executing a program is known as a type error. The notion of type can be lifted from run time (dynamic types) to compile time (static types) in that they are not just a property of data but a property of the program that processes these data. Furthermore this notion of static type can be lifted from each individual program to the programming language in which this program is written. OCaml, for example, is a statically typed programming language in that it is specified not just with a grammar but with typing rules and so to be valid, a program must not only be grammatically correct but type correct too. The genius in this design is that the typing rules are designed in such a way that if a program has a type, then executing it does not give rise to a type error, an achievement due to founding fathers of Computer Science such as Gordon D. Plotkin and Robin Milner, to whom we owe ML and therefore OCaml.
As it turns out, types have a logical content in that their structure is isomorphic to the structure of propositions, a correspondence due to Haskell Curry and William Howard and the motivation for the present lecture notes.
In the same spirit, proofs are not just convincing arguments, they are logical constructs that can be expressed in a language that is just as formally specified as a statically typed programming language, i.e., with a grammar and typing rules.
Our arena of thought here is the Coq Proof Assistant (tCPA for short). This proof assistant features a pure and total functional language, Gallina:
Being total means that unlike OCaml, we cannot write a program whose execution does not terminate.
But then it is very simple to write a terminating program that takes longer than the lifetime of our computer to complete.
Being pure means that unlike OCaml, Gallina features no side effects: no printing (and therefore no tracing), no random numbers, no exceptions, and no mutable data.
And so if we need computational effects, we simulate them:
Since Gallina is a pure and total programming language, as programmers, we cannot detect whether it follows call by value or call by name.
The goal of this first week is to establish a comfort zone for functional programming with Gallina: unit tests, data types, recursive functions, polymorphism, etc.
Created [18 Jan 2024]