Towards the animation of proofs – testing proofs by examples

AbstractIn this paper, we introduce the notion of proof animation, which is a new application of the principle of “Curry–Howard isomorphism” to formal proof development. Logically, proof animation is merely a contrapositive of “proofs as programs”, which is an application of Curry–Howard isomorphism to formal program development. Nonetheless, this new perspective is completely different. The motivation, aims, problems, and a prototype tool under development are presented in this paper. We also discuss possibility of “proof engineering” guided by the Curry–Howard isomorphism