05.07.2025 –, V1 (F119)
Eine Schnupperstunde in Agda, der funktionalen Programmiersprache, mit der man die Korrektheit von Programmcode mathematisch wasserdicht beweisen kann, anstatt auf Tests oder Code-Reviews angewiesen zu sein.
Erwartungsmanagement: Aktuell ist es noch so, dass es sich nur in wenigen Praxisfällen lohnt, den substanziellen Beweisaufwand einzugehen -- auch wenn (nahezu) absolute Korrektheitsgarantie winkt. Diese Whirlwind-Tour dient daher vor allem zur Erweiterung des Horizonts. (Und jede Menge Spaß macht sie auch.)
Hinweis: Um 15:00 Uhr gibt es noch einen weiteren Vortrag zum gleichen Thema. Die beiden Vorträge ergänzen sich -- in Mikes Vortrag geht es um Isabelle, hier geht es um Agda. Beides sind Beweisassistenzsysteme, allerdings mit ziemlich verschiedenen Designprinzipien, Vorteilen und Nachteilen. Beide Vorträge eignen sich zum Reinschnuppern.
Vertrautheit mit mindestens einer Programmiersprache
Mathematiker aus Augsburg
- Wie vollbringen ChatGPT & Co das Kunststück des Lernens?
- Wie funktioniert eigentlich das Internet? Eine Einführung für alle, die gar nicht oder nicht genau wissen, was eine IP-Adresse ist
- Wie eine Gruppe Nerds einen Wald rettete und nur um Haaresbreite vier Wochen Gefängnis entkam
- Drei bizarre philosopho-logische Erzählungen zum Auswahlaxiom, vielleicht dem umstrittensten Axiom der Mathematik