# Intellektik: Technical report 90-01

## Towards a formal theory of program construction

### Christoph Kreitz

A unified framework for formal reasoning about programs *and*
deductive mechanisms involved in programming is developed. Within it
principal
approaches to program synthesis are formally investigated. We will show that
a high degree of abstraction opens a way to combine their strengths,
simplifies formal proofs, and leads to clearer insights into the
meta-mathematics of program construction.
All definitions and theorems are presented completely formal which allows
to straightforwardly implement them with a proof system for the underlying
calculus and derive verified implementations of programming methods
from them.