Wednesday, Jan 4, 2023

About the course

Here we sketch the what, the why, the how, and the why now of this course.


Broadly, our goals are the following

What do these mean?

To make sense of the above, we need to understand:

Such questions form the foundations of mathematics and of computation.

There are different foundational systems, and we will look at two classes of these:

In practice classical foundations are only useful in the small, i.e., for deductions using a relatively small set of axioms.

Indeed real-life mathematics is rigorous in only a local or domain specific fashion – we check that, for instance, calculations involving polynomials are correct in terms of rules and definitions for these, not in terms of polynomials represented in Set Theory.

On the other hand, the foundations building on Dependent Type theory can resemble real-world mathematics as well as form the basis for a real-world programming language.

What do theorem proving programs do?

Theorem proving programs vary in:

They can be used for:


Formalization of mathematics can:


it is arguably worth applying at least the same standards as systems software.


Why now?