Ein Algorithmus soll effizient Lösungen zu gegebenen Problemen berechnen. In der Praxis besteht das Argument, dass der Algorithmus auch die richtigen Lösungen berechnet, meist aus einer Menge von Testfällen, einer kurzen Rechtfertigung in natürlicher Sprache oder einem Stoßgebet. Selbst eine große Menge von Testfällen – auch wenn diese bspw. mithilfe von QuickCheck erstellt wurden – kann aber keine Aussage über die allgemeine Korrektheit eines Softwarestücks machen. Um wirklich sicher zu gehen, müssen wir die Struktur des Codes betrachten, darüber Aussagen treffen und formal argumentieren, dass diese Aussagen auch allgemeine Geltung haben. Ein Mittel, um das zu tun, lernen wir in dieser dreiteiligen Artikelserie kennen: Wir nutzen den SMT-Solver Z3 als automatisierten Theorembeweiser. Diese Artikel sollen einen ersten Einblick geben in die Inhalte unserer neuen iSAQB-Advanced-Level-Schulung zu Formalen Methoden. In der Schulung kommen neben Z3 weitere Verifikationswerkzeuge wie VeriFast, Forge und Liquid Haskell zur Sprache.

Das Programm der Hauskonferenz der Active Group, der BOB 2026, steht: Am Freitag, dem 13.3.2026, findet passenderweise die dreizehnte BOB statt – wie im letzten Jahr im Scandic-Hotel Potsdamer Platz.

Wir sind stolz auf das Programm, für dessen Entstehung wir allerdings viele tolle weitere Einreichungen ablehnen mußten.

Den Eröffnungsvortrag der BOB wird Stefan Kaufmann (stk) halten – es geht um Digitale Souveränität.

Es gibt wie gewohnt vier Tracks – zwei Tracks mit insgesamt 16 Vorträgen, zwei Tracks mit insgesamt 8 Tutorials.

Die Anmeldung ist eröffnet – der Early-Bird-Rabatt läuft noch bis 16. Januar 2026.

Bei der Arbeit am Paper „Evolution of Functional UI Paradigms“, das beim FUNARCH-Workshop der ICFP 2025 veröffentlicht wurde, kam mir ein Gedanke zu puren Funktionen, den ich hier gern separat kurz erläutern möchte. Als Argument für pure Funktionen führen wir funktional Programmierenden gern die bessere Testbarkeit ins Feld: Pure Funktionen erfordern keine komplizierten Test-Setups und Mocks, sind deterministisch, parallelisierbar etc. In der Tendenz ist das sicherlich richtig. Pure Funktionen sind oft besser testbar. Notwendig ist dieser Zusammenhang allerdings weder in die eine noch in die andere Richtung. Es gibt pure Funktionen, die sind schlecht testbar und es gibt auch nicht-pure Funktionen, die gut testbar sind. Die Purity selbst kann also der Stoff nicht sein, der es erlaubt, Programmstücke ordentlich zu testen. Was aber ist dann dieser Stoff?

Am 13. März 2026 findet die BOB, unsere Hauskonferenz über das Beste in der Softwareentwicklung, statt – wieder in Berlin und wieder im Scandic Berlin Potsdamer Platz.

Der Call for Contributions läuft. Schicken Sie uns also (bis zum 17. November 2025) Ihren Vorschlag für einen Vortrag oder ein Tutorial – das Programmkomitee freut sich darauf!

Im vorherigen Artikel dieser Reihe warfen wir einen Blick auf die Programmiersprache Agda. Mit Agda kann man komplexe Spezifikationen ausdrücken und beweisen, dass der Code, den man gegen diese Spezifikationen schreibt, diese auch einhält. Wir hatten das anhand der natürlichen Zahlen und des Zusammenhangs von der Unärdarstellung und der Binärdarstellung illustriert. Zur Erinnerung: Wir hatten die unären natürlichen Zahlen so als Daten beschrieben:

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat