Programs and Proofs: Mechanizing Mathematics with Dependent Types by Ilya Sergey.
From the post:
The picture “Le coq mécanisé” is courtesy of Lilia Anisimova
These lecture notes are the result of the author’s personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.
The primary audience of the manuscript are the readers with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Coq proof assistant, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.
By aiming these two goals, this manuscript is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Coq’s logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the reader a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the “obvious” mathematical intuition.
One approach to change the current “it works, let’s ship” software development model. Users prefer software that works but in these security conscious times, having software that works and is to some degree secure, is even better.
Looking forward to software with a warranty as a major disruption of the software industry. Major vendors are organized around there being no warranty/liability for software failures. A startup, organized to account for warranty/liability, would be a powerful opponent.
Proof techniques are one way to enable the offering limited warranties for software products.
I first saw this in a tweet by Comp Sci Fact.