On the Conciliation of Traditional and Computer-Assisted Proofs

A proof of a mathematical proposition or a program specification obtained by a formal verification process, using an interactive theorem prover, can be questioned as a true demonstration or as having the same purposes of a traditional pencil-and-paper proof. However, in our opinion the verification process of a software component exhibits the same construction phases as a purely mathematical one. A correspondence between both kinds of proofs enables us to give a proposal of what we call transitional proofs, a concept that outlines a conciliation between traditional paper-and-pencil and computer-assisted proofs, which can be useful in philosophical problems surrounding formalized mathematics and program verification with proof-assistants.