Der interaktive Theorembeweiser Isabelle ist nicht nur eine formidable Umgebung, um Mathematik und Logik zu betreiben, sondern auch eine ganz passable funktionale Programmiersprache. In der Kombination dieser beiden Aspekte ergeben sich ungeahnte Möglichkeiten, die Korrektheit eines Algorithmus oder eines Programms zu prüfen. Isabelle kann den verifizierten Code in andere Sprachen (SML, Haskell, Scala) exportieren und so eine eine praktikable Anwendung schaffen.
Auf der Skala der qualitätssichernden Maßnahmen für Computerprogrammen stellt das interaktive Beweisen das eine Extrem da: Maximale Sicherheit, bei großem Aufwand.
In diesem Workshop werden wir ein einfaches funktionales Programm in Isabelle implementieren, und darauf hin interaktiv die Korrektheit des Programms beweisen. Nebenher wird etwas zu den Möglichkeiten und Grenzen von der Arbeit mit Isabelle erzählt.
Installieren Sie bitte Isabelle 2015, und starten Sie es einmal vor dem Tutorial – der erste Start dauert immer etwas länger:
http://isabelle.in.tum.de/installation.html
Grundlegende Kenntnisse in Funktionaler Programmierung sind sehr von Vorteil. Wenn Sie den Haskell-Code auf der ersten Seite des Handouts in etwa verstehen, sollten Sie bestens vorbereitet sein.
Joachim Breitner ist Doktorand am Lehrstuhl für Programmierparadigmen des Karlsruher Instituts für Technologie und forscht zu Haskell, insbesondere zu optimierenden Programmtransformationen und deren Verifikation mit Hilfe des interaktiven Theorembeweisers Isabelle.
Als Hüter der Haskell-Pakete in Debian, als Mitentwickler des Compilers GHC und Mitglied des Haskell Core Library Committees ist er ein aktives Mitglieder der internationalen Haskell-Community. Zuletzt war er an der Einführung der „Safe Coercions“ beteiligt, und die von ihm entwickelte Optimierung „Call Arity“ lässt den Compiler noch mehr Listen mittels list fusion eliminieren. Er betreibt das Haskell performance dashboard, das die Performanceentwicklung des GHCs und anderer Projekte überwacht.
Joachim tanzt Swing und fliegt, wenn das Wetter es erlaubt, Gleitschirm.
