P̶r̶o̶g̶r̶a̶m̶m̶c̶o̶d̶e̶ ̶t̶e̶s̶t̶e̶n̶?̶ Korrektheit beweisen!

11:00 bis 11:50 in Raum V1 (F119)

Ingo Blechschmidt

Abstract

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.

Beschreibung

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.

Vorwissen

Vertrautheit mit mindestens einer Programmiersprache

Über mich

Mathematiker aus Augsburg