Funktionale Programmierung

Die Entwickler:innen-Konferenz BOB 2026 der Active Group am 13.4. war die bisher größte BOB. Hier eine kurze Retrospektive: wie immer haben wir Aufnahmen unserer Talks verlinkt.

Gleichzeitig stimmen wir damit auf die nächste BOB am 26. Februar 2027 ein, natürlich wieder in Berlin. Der Call läuft seit heute noch bis zum 2. November. Schickt uns Eure Ideen zu allem, was am besten ist in der Softwareentwicklung!

Haskell ist eine lazy-evaluierte Sprache. Der GHC-Compiler implementiert diese Semantik, indem Ausdrücke nur so weit evaluiert werden wie ihr Ergebnis tatsächlich gebraucht wird. Im Gegensatz dazu steht die strikte (engl. eager) Evaluation, bei welcher Ausdrücke immer sofort und vollständig ausgewertet werden.

In diesem Artikel wollen wir uns anschauen, welche Vorteile die Laziness mit sich bringt, aber auch welche Fallstricke durch sie entstehen.

In den letzten Monaten haben wir - wie alle in der Branche - viele Gespräche dazu geführt, wie die Zukunft der Softwareentwicklung aussehen wird. Es geht natürlich um „Agentic Engineering“ (AE), also der Benutzung von LLM-basierenden Agenten, um direkt aus Anforderungen den Code für Softwaresysteme zu generieren. Neben der allgemeinen Frage haben wir uns überlegt, was diese Entwicklung für uns bei der Active Group bedeutet und wie wir mit den veränderten Rahmenbedingungen umgehen.

Im ersten Artikel dieser Reihe hatten wir den SMT-Solver Z3 kennen gelernt und uns allgemeine Gedanken zu Spezifikation und Verifikation gemacht. Im zweiten Artikel haben wir den sogenannten Bresenham-Algorithmus – eine Berechnungsvorschrift zum Zeichnen von geraden Linien – mit Z3 implementiert und dann auch sichergestellt, dass dieser Algorithmus genau das tut, was wir von ihm erwarten. Die Implementierung des Bresenham-Algorithmus in Z3 ist zwar lauffähige Software, allerdings ist Z3 (bzw. SMT-LIB2) keine Allzweckprogrammiersprache, d.h. wir werden kein umfängliches Softwareprojekt komplett in Z3 schreiben können. War also alles letztlich doch für die Katz?

Im ersten Artikel dieser Reihe hatten wir den SMT-Solver Z3 kennen gelernt. Wir hatten in der zugehörigen Sprache SMT-LIB-2 eine Spezifikation für die Rasterisierung von Geraden verfasst und dann einen verbesserten Algorithmus entworfen, der mit dem Simplen in seiner Funktionsweise übereinstimmt. Während die Korrespondenz dieser beiden Algorithmen manchen Lesern vielleicht noch offensichtlich erschien, gehen wir in diesem Artikel einen signifikanten Schritt weiter. Wir implementieren den sog. Bresenham-Algorithmus, bei dem auf den ersten Blick ganz und gar nicht mehr klar ist, warum er überhaupt funktioniert.