Curiously Empty Intersection of Proof Engineering and Computational Sciences

Abstract

The tools and techniques of proof engineering have not yet been applied to the computational sciences. We try to explain why and investigate their potential to advance the field. More concretely, we formalize elementary group theory in an interactive theorem prover and discuss how the same technique could be applied to formalize general computational methods, such as discrete exterior calculus. We note that such formalizations could reveal interesting insights into the mathematical structure of the methods and help us implement them with stronger guarantees of correctness. We also postulate that working in this way could dramatically change the way we study and communicate computational sciences.