# Intellektik: Technical report 94-07

## A Foundation for Verified Software Development Systems

### C. Kreitz

We describe a formalization of the meta-mathematics
of programming in a
higher-order calculus as a means to create verifiably correct
implementations of program synthesis tools. Formal definitions and
lemmata are used to raise the level of abstraction in formal reasoning
to one comprehensible for programmers. Formal meta-theorems make
explicit the semantic knowledge contained in program derivation
*methods* and serve as kernel of derived inference rules implementing
these methods. By an example formalization of a strategy deriving
global search algorithms we demonstrate the advantages of combining
formal mathematics with an interactive theorem proving environment to
develop powerful, flexible, and reliable systems for knowledge-based
software development. We describe a formalization of the
meta-mathematics of programming in a
higher-order calculus as a means to create verifiably correct
implementations of program synthesis tools. Formal definitions and
lemmata are used to raise the level of abstraction in formal reasoning
to one comprehensible for programmers. Formal meta-theorems make
explicit the semantic knowledge contained in program derivation
*methods* and serve as kernel of derived inference rules implementing
these methods. By an example formalization of a strategy deriving
global search algorithms we demonstrate the advantages of combining
formal mathematics with an interactive theorem proving environment to
develop powerful, flexible, and reliable systems for knowledge-based
software development.