Im Endeffekt ist Softwareentwicklung ein logischer Schlussfolgerungsprozess, in dem Wissen über Programme, Anwendungsbereiche und Programmiermethoden verarbeitet wird. Diesen Prozess durch Computer zu unterstützen verlangt eine verständliche Formalisierung aller in den Softwareentwicklungsprozess verwickelten Komponenten in einem formalen logischen Kalkül. Das niedrige Abstraktionsniveau solcher Kalküle hat bisher jedoch den wissenschaftlichen Fortschritt in der Programmsynthese erheblich erschwert.

Der Vortrag stellt ein theoretisch-formales Fundament für eine systematische Entwicklung von Programmsynthesesystemen vor. Ausgangspunkt ist eine einheitliche Formalisierung der Objekt- und Meta-Theorie der Programmierung. Eigenschaften deduktiver Methoden zur Softwareentwicklung und der von ihnen erzeugten Programme kánnen dann als Theoreme in dem formalen Kalkül ausgedrückt und bewiesen werden. Führt man dies mit einem rechnergestützten Beweissystem für den Kalkül aus, so liefern die formalen Beweise verifizierte Implementierungen von Programmsyntheseverfahren. Dies wird im Vortrag am Beispiel von Syntheseparadigmen und konkreten Synthesestrategien illustriert werden.