Die International Conference on Functional Programming (ICFP) ist alljährlich die größte internationale Konferenz zur funktionalen Programmierung, so auch dieses Jahr, wo die ICFP in Göteborg stattfand. Seit letztem Jahr ist die ICFP größer als die OOPSLA, ihr Pendant in der objektorientierten Welt. Um die ICFP herum gibt es inzwischen einen ganzen Zoo von Satellitenveranstaltungen, von High-Performance-Computing bis Kunst - allesamt mit dem einenden Thema der funktionalen Programmierung.

Dieser Artikel enthält einen Rückblick auf einige Highlights.

Über alle Aspekte der ICFP zu berichten ist aufgrund der Themenvielfalt und schieren Anzahl der Vorträge ein hoffnungsloses Unterfangen. Glücklicherweise sind nahezu alle Vorträge auf YouTube zu sehen - wer Zeit hat, kann sich also umfassend informieren.

ICFP

Generell ist in der funktionalen Programmierung der Trend zu beobachten, von der funktionalen Modellierung zur nächsten Stufe der Softwareentwicklung vorzudringen, bei der Compiler und Programmiersysteme helfen, die Korrektheit von Programmen sicherzustellen.

Wie große Bedeutung dieses Thema hat, machte Kathleen Fishers Keynote (dazu gibt es leider kein Video) klar. Es geht um high-assurance vehicles - Hubschrauber und Autos, die ohne Computer und Software inzwischen gar nicht mehr funktionieren würden. Leider wird bei der Entwicklung dieser Software bislang nur wenig Augenmerk auf die Sicherheit gelegt, so dass gängige Kontrollsoftware für autonome Flugkörper und handelsübliche Autos mit erschreckender Leichtigkeit von Angreifern übernommen werden können. Kathleen Fisher hat das DARPA-Programm HACMS geleitet, das Softwaretechnologie entwickelt, um solche high-assurance vehicles sicher vor Angriffen zu machen. Dazu kommt - natürlich - funktionale Programmierung, zum Beispiel in Form von automatischen Beweisern wie Isabelle oder des korrekt bewiesenen C-Compilers CompCert zum Einsatz.

Auch in Robby Findlers Keynote ging es darum, wie ein Entwickler sicherstellen können, dass ihre Softare korrekt funktioniert. Robby Findler hat die formale Forschung zu Contracts begründet, die es erlaubt, Invarianten als Verträge zwischen Programmkomponenten im Programm abzulegen und dort automatisch zu verifizieren.

Während Contracts dynamisch funktionieren (auch wenn es die ersten Bemühungen gibt, die Überprüfung statisch vorwegzunehmen), gibt es immer mehr Arbeiten zur statischen Verifikation, vor allem unter Benutzung von Dependent Types. Gleich mehrere im Vormarsch befindliche Programmiersysteme aus dem Umfeld der funktionalen Programmierung - darunter Coq, Agda und Idris - machen dies mit mächtigen Typsystemen, die Dependent Types unterstützen, also die Verschmelzung der Programmierung auf Typ- und Wertebene. Dependent Types sind ein mächtiges Werkzeug, um auch komplexe Programmeigenschaften direkt im Programm zu notieren und automatisch verifizieren zu lassen. Stephanie Weirichs Keynote beschreibt ihr Projekt, Dependent Types auch in Haskell zu implementieren.

CUFP

Auch auf der Konferenz Commercial Users of Functional Programming gab es wieder viele erstaunliche Vorträge, die allesamt auf YouTube verewigt sind. Auffällig waren dieses Jahr die Vorträge zu Haskell im Weltraum.

Wie in jedem Jahr gab es auf der CUFP wieder viele Tutorials von Korifäen des Fachgebiets, so zum Beispiel zu Dependent Types (s.o.) in Agda und Idris. Auch Funktionale Programmierung war mit einem Tutorial zu Haskell vertreten.

FARM

Schon zum zweiten Mal fand dieses Jahr der Workshop on Functional Art, Music, Modeling and Design (FARM), der sich vor allem mit der Modellierung von Musik mit funktionaler Programmierung beschäftigt. Dabei gibt es insbesondere eine starke Live-Coding-Gemeinde, die Musik vor den Ohren der Zuschauer programmiert. Die Videos zur FARM rollen gerade noch ein. Entsprechend bildete auch ein ganzer Abend von Live-Coding-Performances einen würdigen Abschluss für die ICFP.

Haskell Symposium und Implementors Workshop

Haskell war mit Veranstaltungen an drei Tagen vertreten: zunächst ging es auf dem Haskell Symposium zwei Tage lang um theoretische Grundlagen und Spracherweiterungen. Auch hierzu gibt es reichlich Videomaterial. Danach ging‘s auf dem Haskell Implementors Workshop weiter mit technischen Details zu den neuesten GHC-Erweiterungen und zu anderen Compiler-Hacks. Die Videos hierzu sind auch bereits online.