Program calculation is a family of techniques for deriving programs from their specifications. Unlike other approaches, where correctness is verified through proofs or tests that are extrinsic to the program, calculational approaches aim to provide correctness-by-construction, where the correctness of the program follows from the validity of the steps used to produce it.
In this course, we will survey a number of different approaches to calculating programs, all operating at different levels of formality and having differing strengths and weaknesses. We will show how to use these techniques on a number of simple examples, culminating in a longer, more drawn-out example with real-world applicability.
This course assumes a basic knowledge of the principles of functional programming. Other necessary concepts will be introduced as we go.