Building reliable software is hard. The developing of large-scale systems are prone to bugs and insecurities. Computer scientists have responded these challenges for improving reliability, using mathematical techniques for specifying and reasoning about properties of software and tools for helping validating these properties. The Software Foundations series is focused on this last set of tools.
This course is based around Coq, which enables a variety of works:
As a platform for modeling programming languages.
As an environment for developing formally certified software and hardware.
As a realistic environment for functional programming with dependent types.
As a proof assistant for higher-order logic.
The most basic programming style is to keep the computations pure as much as possible, avoiding side effects such as changes of local states; this makes the programs easier to understand and reason about.
Coq is a proof assistant yet a functional programming language. These two sides of Coq are the reflection of the underlying machinery, that is, proofs are programs.
Chapter 1 Functional Programming in CoqChapter 2 Proof by InductionChapter 3 Working with Structured DataChapter 4 Polymorphism and Higher-Order FunctionsChapter 5 More Basic TacticsChapter 6 Logic in CoqChapter 7 Inductively Defined PropositionsChapter 8 Total and Partial MapsChapter 9 The Curry–Howard Correspondence