Spaß mit Agda

Matthias und Ingo veranstalten eine Agda-Sitzung, sicherlich gespickt mit zahlreichen hintergründigen Kommentaren und Ergänzungen von Makarius.

Was ist Agda? Agda ist eine abhängig typisierte funktionale Programmiersprache und ein Beweisassistent.

Was ist die Verbindung zu Isabelle? Isabelle ist viel, viel größer. Beweisautomatisierung ist in Agda extrem unterentwickelt. Isabelle kann noch viel, viel mehr als nur Beweise zu prüfen. In Isabelle schreibt man standardmäßig Beweistexte, während man in Agda direkt Beweisterme angibt. (Dieser Unterschied wird in der Agda-Sitzung erklärt werden.) Der theoretische Unterbau von Agda ist ein ganz anderer als der von Isabelle/HOL (ein Typensystem mit abhängigen Typen statt HOL). Die Community von Agda nerdet meist konstruktiv ab, während die Community von Isabelle sich meist klassische Logik gönnt. Mit Agda kann man auch Homotopietypentheorie (HoTT) betreiben, mit Isabelle/HOL nicht (wohl aber mit reinem Isabelle). Mit Agda kann man in die wundersame Welt prädikativer Mathematik eintauchen. In Agda gibt es den Begriff “universe polymorphism”, den Ingo persönlich sehr verlockend findet.

Von wem ist Agda? Agda wurde von Catarina Coquand auf den Weg gebracht, der Ehefrau von Thierry Coquand, der wiederum die theoretische Basis zur weiteren Theorembeweiseralternative Coq entwickelte. Wir kennen kein weiteres Ehepaar, das von sich behaupten kann, zwei große Theorembeweiserschulen gegründet zu haben.

Wer kann sich besonders auf die Agda-Sitzung freuen? Jede, die verstehen möchte, inwieweit Beweisen und Programmieren ein und dasselbe sind. Jede, die mehr Erfahrung mit abhängigen Typen sammeln möchte. Jede, die (wie etwa Richi vor einiger Zeit) mal aufschnappte, dass manche Ansammlungen in der Mathematik zu groß sind, um “Mengen” zu bilden und stattdessen nur “echte Klassen” sind, und gerne wüssen würde, was es damit auf sich hat. Jede, die sich über einen einfachen Einstieg in die Welt computergeprüfter Beweise freut.

Welche Voraussetzungen setzt die Agda-Sitzung voraus? Keine außer etwas Vertrautheit mit Programmieren.