Chapter 1: Computer-Checked Proofs and Formal Methods

The first chapter of the Iowa Type Theory Commute is about computer-checked proofs for Mathematics and Computer Science. Computer-checked proofs give us a new level of certainty about theorems, not possible in previous human history, and these theorems can be about software. This enables us to reach previously unjustifiable levels of confidence in the correctness of software. Adoption of these techniques has been very slow among Mathematicians, and more zealous among Computer Scientists. The power of these formal methods is great, but applying them is costly, so engineering considerations are important.