Constructive Programming: A Personal View

摘要

Constructive programming is a kind of formal method for functional programming; its aim is to develop verified programs through the creation of formalized proofs that use constructive mathematics. This paper is a personal perspective of the research area. It consists of four parts: a brief account of formal methods, an account of constructive programming, correspondences between these two areas, and a conclusion. An appendix contains some recent thoughts that were added after the body of the paper was finished.