# Intellektik: Technical report 93-13

## Formal Mathematics for Verifiably Correct Program Synthesis

### Christoph Kreitz

We describe a formalization of the meta-mathematics of
programming as a means to implement verifiably correct tools for
program synthesis. We demonstrate the advantages of using formal
mathematics as support for AI-techniques by an example formalization
of a strategy deriving global search algorithms from specifications.