Formal Mathematics for Verifiably Correct Program Synthesis

We describe a formalization of the meta-mathematics of programming in a higher-order logical calculus as a means to create verifiably correct implementations of program synthesis tools. Using reflected notions of programming concepts we can specify the actions of synthesis methods within the object language of the calculus and prove formal theorems about their behavior. The theorems serve as derived inference rules implementing the kernel of these methods in a flexible, safe, efficient and comprehensible way. We demonstrate the advantages of using formal mathematics in support of program development systems through an example in which we formalize a strategy for deriving global search algorithms from formal specifications. Keywords: Program Synthesis, Type Theory, Reflected Reasoning 1 Introduction For more than twenty years commercial software production has been in a state of endemic crisis. The crisis is caused by the property which makes software attractive: the complexity of beh..