Funktionale Programmierung

In den drei Artikeln zum Z3-Theorembeweiser (1, 2, 3) haben wir uns mit der Korrektheit des Bresenham-Linienzeichen-Algorithmus befasst. Wer Korrektheit sagt, muss auch Spezifikation sagen, denn korrekt kann ein Algorithmus immer nur im Bezug auf eine eindeutige Beschreibung des gewünschten Verhaltens sein. Als Spezifikation hatten wir in SMT-LIB2 (der Sprache von Z3) einen simplen (aber langsamen) Referenzalgorithmus beschrieben. Wir haben dann den komplexen (aber effizienten) Bresenham-Algorithmus implementiert und bewiesen, dass dieser dasselbe Verhalten aufweist wie der simple Algorithmus. Referenzalgorithmen als Werkzeuge zur Formulierung von Korrektheitsaussagen haben den Vorteil, dass sie oft einfach zu finden sind. Der Spezifikationsaufwand hält sich so in Grenzen. Es geht aber auch anders. Mit mehr Aufwand findet man manchmal elegantere Spezifikationen, die beispielsweise flexibler sind (d.h. standhafter im Angesicht von Anforderungsänderungen) oder den Beweisaufwand signifikant verringern.

In diesem Artikel wollen wir uns das Thema Linienzeichnen noch einmal vornehmenen und uns dabei einzig und allein auf die Spezifikation konzentrieren. Mit SMT-LIB2 stoßen wir dabei allerdings schnell an die Grenzen der Ausdrucksfähigkeit. Wir verwenden deshalb für diesen Artikel den Theorembeweiser bzw. die Programmiersprache Agda, die auf diesem Blog schon eingeführt wurde. Wir werden die wichtigen Merkmale von abhängigen Typen (Dependent Types) – dem wesentlichen Feature von Agda – in diesem Artikel so einführen, dass man aber auch ohne Vorerfahrung folgen kann. Aber Vorsicht: Vom Umgang mit abhängigen Typen wird man manchmal selbst süchtig.

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?