The Computational Relevance of Formal Logic Through Formal Proofs

摘要

The construction of correct software, i.e. a computer program that meets a given specification, is an important goal in Computer Science. Nowadays, not only critical software (the ones used in aircraft, hospitals, banks, etc.) is supposed to provide additional guarantees of its correctness. Nevertheless, this is not an easy task because proofs are often long and full of details. In this sense, a strong background in logical deduction is essential to provide Computer Science (CS) professionals the necessary competencies to understand and provide mathematical proofs of their programs. Logic courses for CS tend to follow old precepts without emphasizing mastering deduction itself. In our institution, for several years we have followed a more pragmatical approach, in which the foundational aspects of both natural deduction and deduction a la Gentzen are taught and, in parallel, the operational premises of deduction are put into practice in proof assistants. Thus, CS students with a minimum knowledge in programming are challenged on providing correctness certificates for simple algorithms. 'Putting their hands in the dough' they acquire a better understanding of the value and importance of deductive technologies in computing. Here we show how this is done relating natural deduction and sequent calculus deduction and using the proof assistant PVS in the simple context of a library of sorting algorithms.