Dieses Problem kann dadurch gelöst werden, dass auf der Basis von Typentheorie eine formale Theorie der Programmierung entwickelt wird, welche in der Begriffsbildung den aus Standardlehrbüchern bekannten Programmierkonzepten entspricht und ein logisches Schliessen auf diesem Niveau unterstützt. Da man sich auf diese Art von den Eigenarten einer speziellen Formulierung der Typentheorie lösen kann, werden Inferenzen und Synthesen einfacher, "natürlicher" und verständlicher. Durch die Abstützung auf Typentheorie bleiben sie aber dennoch vollständig formal und verifizierbar korrekt. Die Formalisierung der Theorie der Programmierung bildet daher das Fundament einer praktisch verwendbaren Inferenzmaschine für wissensbasierte Software-Entwicklung.

Neben der Formulierung von Faktenwissen über verschiedene Standardanwendungsbereiche (das sogenannte Objektwissen) bildet die Formalisierung deklarativen Wissens über Programmentwicklungsmethoden (Metawissen) einen zentralen Bestandteil dieser Theorie. Letztere ermöglicht es, eine verifizierte Implementierung von Syntheseverfahren auf der Basis von Theoremen durchzuführen, welche die zentralen Eigenschaften in einer Art formalisieren, die der heute üblichen Beschreibungsform auf dem Papier sehr nahe kommt. Fehler beim ębergang von der Beschreibung der Strategie zur Codierung sind somit ausgeschlossen. Zudem erlaubt die deklarative Charakterisierung auf hohem Abstraktionsniveau den Vergleich und die Integration von Verfahren, die aufgrund der der verschiedenartigen Formalismen, in denen sie entworfen wurden, bisher nur schwer verglichen werden konnten.

Auch wenn die Entwicklung einer vollständigen formalen Theorie der Programmierung ein Langzeitprojekt ist, bei dem vor allem auch Wert auf die Festlegung von Standards für Begriffsbildungen gelegt werden muss, ist ihr zentraler Kern bereits erstellt und durch die Untersuchung einiger Syntheseverfahren exemplarisch getestet worden. Im Vortrag wurde dies illustriert anhand eines Theorems über die konstruktive Äquivalenz der drei Hauptparadigmen der Programmsynthese (Beweise als Programme, Transformationen, Algorithmenschemata) und der Formalisierung einer Strategie zum Entwurf von Globalsuch-Algorithmen aus ihren Spezifikationen.