| Formal methods are a class of techniques for automatically verifying software correctness. They are a common topic in computer science research. However, they are less well-known in software development and in undergraduate computer science education.;As society's reliance on software increases so does the potential severity of the consequences of software failure. Formal methods are the surest way of guaranteeing software correctness. Moreover, the study of formal methods leads to better informal understanding of software correctness and thus to better software.;Unfortunately, the study and use of formal methods can be difficult and this impedes their adoption in software engineering and the computer science curriculum. Coq is an automated proof-assistant for developing certified programs and proofs. It is powerful and expressive and has been used in a large variety of significant developments.;Experienced developers are accustomed to picking up new languages rapidly. Unfortunately, it is difficult for a new user to learn the use of any proof-assistant with anything like the same rapidity. Furthermore, developers have become accustomed to sophisticated IDEs with tools for refactoring and for auto-generating code. Very little such support is available for proof-assistants. Coq suffers from both these drawbacks.;Our work addresses these problems in several ways. We provide two alternative approaches that facilitate general induction and recursion. We demonstrate methods for enhancing structural recursion principles to increase their generality and transparency. We demonstrate graphical techniques for improved proof visualization and an impact analysis tool for predicting the consequences of a proof refactoring. |
