Richard A. De Millo, Richard J. Lipton und Alan J. Perlis – 1979
Viele Menschen argumentieren, dass das Programmieren stärker der Mathematik ähneln sollte. Vielleicht stimmt das – aber nicht in der Weise, wie sie es sich vorstellen. Das Ziel der Programmkontrolle, eines Versuchs, das Programmieren mathematischer zu gestalten, besteht darin, das Vertrauen in die korrekte Funktionsweise eines Softwarestücks erheblich zu erhöhen. Das Mittel, das Verifikatoren dafür nutzen, ist eine lange Kette formaler, deduktiver Logik. In der Mathematik besteht das Ziel darin, das Vertrauen in die Korrektheit eines Theorems zu stärken, und es stimmt, dass eine lange Kette formaler Logik theoretisch eines der Werkzeuge sein könnte, um dieses Ziel zu erreichen. Doch in der Praxis ist das nicht der Fall. Mathematiker verwenden stattdessen einen Beweis – etwas völlig anderes. Ein Beweis beendet die Debatte jedoch nicht endgültig; entgegen seines Namens ist er lediglich ein Schritt in Richtung Vertrauen. Letztlich, so glauben wir, ist es ein sozialer Prozess, der darüber entscheidet, ob Mathematiker Vertrauen in ein Theorem haben. Und weil ein vergleichbarer sozialer Prozess unter Programmverifikatoren nicht stattfinden kann, ist Programmkontrolle zum Scheitern verurteilt. Wir sehen nicht, wie sie das Vertrauen in Programme tatsächlich beeinflussen könnte.
(Eigene Übersetzung des Abstracts von Springer Nature)
DOI des Kapitels: https://doi.org/10.1007/978-94-011-1793-7_14