0.1: Course Overview

This course is based on the following philosophical principle:

All computing scientists must be able to employ rigorous reasoning to justify their claims about the behaviour of the programs they produce.

Thus the goal of this course is to introduce you to the logical and mathematical tools for reasoning about algorithms. Being able to effectively use these tools makes the difference between being a programming hack and a computing scientist. However, a course such as this can only examine the elementary material.

We will be covering in depth a small number of essential ideas. The course contains three main parts:

  1. Reasoning about programs. Throughout the course we will be looking at programs as formal objects. Our goal will be to precisely specify the behaviour we wish our programs to have, and then to develop programs and prove that they have the desired behaviour.
  2. A formal system for predicate logic. In this part we will introduce and use a formal system for predicate logic. Unlike previous versions of this course, and many courses on logic, we will not be using a system that exists only on paper. Instead we will be writing proofs that can be checked for correctness using the Mizar MSE system. In much the same way that you write a program, you will be entering your proofs into files and running them through Mizar. By the end of this part of the course you should be very comfortable with the idea of a proof, how to read one, and to some extent, how to write one.
  3. Basics: Sets, Relations, Functions, and Induction. This could have been the first part of the course. We will introduce as required, various concepts such as sets, relations, functions, types, induction, and basic number theory.

NOTE: Parts 1 and 3 above are not included in this document. -- FL