HIP 5

Agda ist ein Beweisassistent – also ein Werkzeug, mit dem man z.B. mathematische Aussagen oder die Korrektheit von Programmen beweisen kann. In diesem Workshop werfen wir einen Blick darauf, wie das überhaupt funktioniert und probieren es aus. Wenn man schonmal programmiert hat, ist das gar nicht so schwierig wie man vielleicht denkt – Agda ist nämlich eigentlich nur eine (funktionale) Programmiersprache.

Das Ziel des Worshops ist es, dass ihr ein Verständnis davon erlangt, wie Beweise und Programme zusammenhängen. Das nennt man auch die Curry-Howard-Korrespondenz. Gerade für Leute, die zwar gerne programmieren, aber bisher um theoretische Informatik, Mathematik und Beweise einen Bogen gemacht haben, ist das vielleicht ein spannender neuer Zugang zu diesen Themen, der Lust auf mehr macht!

Vorkenntnisse im Beweisen oder funktionaler Programmierung sind nicht nötig. Nur allgemeine Programmierkentnisse (z.B. was eine Funktion oder ein Datentyp ist, Sprache ist aber egal) und den Umgang mit dem Editor setze ich voraus.

Wenn ihr live mithacken wollt, bringt gerne einen Laptop mit. Am Besten installiert ihr euch vorher schon Agda und ein passendes Editor-Plugin. Am einfachsten ist es vermutlich, das VS-Code-Plugin zu installieren und dort den Language Server einzuschalten – das Plugin sollte dann den Rest automatisch herunterladen. Agda-Plugins gibt es aber z.B. auch für emacs und vim.

Hier geht es zum Repo mit dem Agda-Code vom Workshop mit stichwortartigen Erklärungen.