Position Paper: Thoughts on Programming with Proof Assistants

Today the reigning opinion about computer proof assistants based on constructive logic (even from some of the developers of these tools!) is that, while they are very helpful for doing math, they are an absurdly heavy-weight solution to use for practical programming. Yet the Curry-Howard isomorphism foundation of proof assistants like Coq [Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004] gives them clear interpretations as programming environments.My purpose in this position paper is to make the general claim that Coq is already quite useful today for non-trivial certified programming tasks, as well as to highlight some reasons why you might want to consider using it as a base for your next project in dependently-typed programming.