Die Typentheorie: Ein Ausblick in die Zukunft der Software-Entwicklung

Die Datentypen von streng typisierten Programmiersprachen wie ML und Haskell können wie folgt mit der Logik in Bezug gebracht werden.

Zu einem einer Funktion kann eine Spezifikation in der Form einer logischen Formel gegeben werden. Für eine Funktion quicksort, die eine Liste von ganzen Zahlen aufsteigend sortiert, könnte eine solche Spezifikation die  Aussage A sein, dass die Ergebnisliste aufsteigend sortiert ist. Die Funktion quicksort erfüllt ihre Spezifikation A genau dann wenn, sie einen Beweis davon ist, dass jede Liste von ganzen Zahlen aufsteigend sortiert werden kann.

Der Ansatz verlangt, dass der Beweisbegriff so eingeschränkt ist, dass nur Beweise betrachtet werden, die Algorithmen sind. Man spricht in der Logik von „konstruktiven Beweisen„. Damit sind Beweise gemeint, die die Objekte explizit aufbauen, deren Existenz sie zeigen, und im Falle von Alternativen (wie etwa eine Zahl ist gerade oder ungerade) immer klarstellen, welche Alternative bewiesen wird. Widerspruchsbeweise zum Beispiel erfüllen diese Bedingungen nicht und werden folglich beim Ansatz nicht zugelassen.

Nach diesem Ansatz liefert also die ganz oder teilweise  automatische Suche nach Beweise (von Spezifikationen), wenn sie gelingt, Algorithmen (in der Form von Funktionen). Somit verspricht der Ansatz die (Teil-)Automatisierung der Programmierung. Diese Aussicht ist von gewaltigen Tragweite – nicht nur für die Theorie, sondern auch und vor allem für die Praxis der Software-Entwicklung. Die Software-Entwicklung könnte damit von einer Kunst, die schwer zu erlernen ist und zeitaufwendig ist, zu einer (teil-)automatische Arbeit, also zu einer Arbeit, die durch Software zumindest zum Teil zu bewältigen wäre.

Die Spezifikation einer Funktion in der Form einer logischen Formel kann zudem als Typ dieser Funktion angesehen werden, weil sie statisch (das heißt zur Übersetzungszeit und unabhängig von den Eingabeparametern) überprüft werden kann.

Der hiermit kurz geschilderter Ansatz wird in der sogenannten „Typentheorie“ untersucht, die ein der spannendsten Gebieten der derzeitigen Theoretischen Informatik ist. Die Auslegung von logischen Spezifikation als Typen von Funktionen wird „Curry-Howard-Isomorphismus“ genannt.

Der Ansatz sieht zweifelsohne wie Science Fiction aus. Man sollte sich aber nicht täuschen. So sah auch die statische Typprüfung Anfang der 70er Jahren des 20. Jahrhundert aus oder in den 60er Jahren des 20. Jahrhundert die Vison einer Software, die Schach-Weltmeister schlagen könnte. Es steht außer Frage, dass aus dem Curry-Howard-Isomorphismus und der Typentheorie praktische Werkzeuge der Programmierung und Software-Entwicklung früher oder später entstehen werden.

FB

6 Responses to “Die Typentheorie: Ein Ausblick in die Zukunft der Software-Entwicklung”

  1. dasuxullebt sagt:

    Sicherlich wird es an Bedeutung gewinnen, allerdings gibt es das Problem, dass das mathematische Beweisen an sich schon eine recht schwierige Angelegenheit ist. Hinzu kommt, dass rein mathematische Beweise oft extrem schlechte Algorithmen enthalten, wenn sie denn überhaupt konstruktiv oder konstruktivierbar sind. Und die Algorithmen, bei denen man wirklich einen Beweis haben will, sind im Allgemeinen auch Zeit- und Speicherkritisch.

    Das heißt, man braucht hier Leute, die sowohl konstruktive mathematische Beweise verfassen können, als auch Ahnung von Algorithmik haben, als auch ziemlich elementare Optimierungen beherrschen. Freilich gibt es solche Menschen, aber es gibt Wenige, und damit sind solchce Leute teuer.

    Im Allgemeinen werden Systeme momentan aber eher darauf optimiert, dass man viele möglichs billige Arbeitskräfte davorsetzen kann. Es wird also schwierig.

  2. FB sagt:

    @dasuxullebt: Das sehe ich ein bisschen anders. Theorembeweiser sind sicherlich komplexe Systeme. Betriebssysteme, Web-Browser und Flugzeuge auch. Das hindert nicht daran, dass es sie gibt und dass viele Menschen sie benutzen, die keine Ahnung davon haben, wie sie aufgebaut werden.

    Ich glaube auch nicht, dass man unbedingt Logik-Kenntnisse und Kenntnisse der konstruktiven Logik haben muss, um den Ansatz nach dem Curry-Howard-Isomorphismus zu nutzen. Im Gegenteil. Es dürfte weitgehend wie die Programmierung in streng typisierten Sprachen sein: Sie ist auch für Menschen gut möglich, die den Unifikationsalgorithmus (zur statischen Typprüfung) nicht kennen.

  3. dasuxullebt sagt:

    Bei Browsern und Betriebssystemen hackt man aber einfach so lange drauf rum, bis das System das macht, was man will.
    Ich denke eher, dass automatische Assertion-Checks eine Zukunft im Mainstream haben.

  4. FB sagt:

    @dasuxullebt: Vieles in der Programmierung ist Routine und verlangt keine ausgeklugten Algorithmen. Wo solche benötigt werden, werden in der Praxis meist im Voraus definierten Algorithmen. Deswegen bin ich optimistisch, was den praktischen Ertrag des Curry-Howard-Isomorphismus angeht. Darunter fallen auch automatische Assertion-Checks, die höchstwahrscheinlich eine große Zukunft haben dürften.

  5. FB sagt:

    @dasuxullebt: Vieles in der Programmierung ist Routine und verlangt keine ausgeklugten Algorithmen. Wo solche benötigt werden, werden in der Praxis meist im Voraus definierten Algorithmen. Deswegen bin ich optimistisch, was den praktischen Ertrag des Curry-Howard-Isomorphismus angeht. Darunter fallen auch automatische Assertion-Checks, die höchstwahrscheinlich eine große Zukunft haben dürften.

  6. Andreas sagt:

    Diese positive Rezension der Typentheorie freut mich natuerlich. Viel Arbeit wird noch erforderlich sein, um den Ansatz praxistauglich zu machen, insbesondere Beweis(teil)automation.

Leave a Reply