07.03, 14:00–16:00 (Europe/Berlin), Vortragssaal
Ein kleiner Einblick in die Welt des Beweisen und Programmieren mit Agda!
Agda ist ein Beweisassistent: 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 funktioniert und probieren es live aus. Wenn man schonmal programmiert hat, ist das gar nicht so gruselig, wie es vielleicht klingt – Agda ist nämlich eigentlich nur eine (funktionale) Programmiersprache.
Unser Ziel für diesen Einstieg ist, gemeinsam ein erstes Verständnis davon zu erlangen, dass Beweise und Programme im Grunde dasselbe sind. Diese Erkenntnis nennt man auch 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 hoffentlich ein spannender neuer Zugang zu diesen Themen, der Lust auf mehr macht!
Vorkenntnisse im Beweisen oder in 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 richtet ein passendes interaktives Editor-Plugin ein. Das Plugin für VS Code z.B. kann Agda sogar direkt automatisch installieren. Plugins gibt es aber z.B. auch für emacs und vim.
Die Workshop-Materialien gibt es in einem öffenltichen Git-Repo.
