Proofs of Correctness in Mathematics and Industry
Henk P Barendregt · Wiley Encyclopedia of Computer Science and Engineering · 2007
Abstract Quality of a product needs verification. If the product is complex, this verification cannot be done “by hand,” but one needs tools. The question then arises how those tools are being checked. Eventually quality comes from a careful specification and design methodology. Correctness is based on a mathematical proof that the design meets its specification. As mathematical proofs become long and complex themselves, we also need a tool to verify proofs. In order to prevent an infinite regress, this last tool must have a basic simplicity. Indeed, mathematical assistants that help users to develop and verify proofs are build on the current foundational logical systems that can be described in a couple of pages. It is expected that within a couple of decades, the use of reliable mathematical assistants will be widespread and will help the human user to learn, develop, teach, communicate, referee, and apply mathematics. Computer‐verified correctness will probably become one of the most important applications of mathematics and computer science.