Startschuss für die BOB 2025!

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

Die Keynote hält Annette Bieniusa!

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

Eine Neuerung gibt‘s gleich am Anfang: Es gibt bereits ab jetzt vergünstigte Katze-im-Sack-Tickets für 160 €. Wer sich also jetzt schon für den Besuch der BOB entscheidet, ist klar im Vorteil. Diese Tickets gibt es noch bis zur Bekanntgabe des Programms am 11. Dezember.

Weiterlesen...

Wie lernt man am besten Agda – Eine Quellen­sammlung

Im letzten Artikel der Denotational-Design-Reihe hatten wir die Programmiersprache bzw. den Theorembeweiser Agda kennen gelernt. In diesem kleinen Einschub stelle ich einige Ressourcen vor, mithilfe derer man seine Agda- und Dependent-Typing-Skills vertiefen kann. Ich stelle die Ressourcen in einer Reihenfolge vor, von der ich denke, dass sich diese für mich gut zum Lernen geeignet hätte.

Weiterlesen...

BOB 2024 – Retrospektive

Am 15.03.2023 feierte die BOB, unsere alljährliche Entwickler:innenkonferenz, ihre elfte Ausgabe. Diesmal im Scandic-Hotel Potsdamer Platz, Berlin, eine Location, die einige schon von der SommerBOB 2019 kannten. Bereits am Vorabend hatten sich die ersten zu einem lockeren Austausch bei Pizza und Bier getroffen – vielen Dank an dieser Stelle an NewStore GmbH für die Einladung und die Organisation!

Weiterlesen...

Einführung in Denotational Design, Teil III: Einführung in Agda

Dieser Artikel ist der dritte einer Reihe über Denotational Design. In diesem Artikel lernen wir Agda kennen. Agda ist eine Programmiersprache mit einem sehr ausdrucksstarken Typsystem. Es lassen sich mit Agda fast beliebige formale Aussagen als Typen ausdrücken. Implementierungen – Werte dieser Typen – werden dadurch zu Beweisen, die zeigen, dass diese Aussagen auch zutreffend sind. Wir legen uns im Folgenden das Beispiel mit den binären Numeralen aus dem ersten Artikel vor und formalisieren es in Agda. Im nächsten Artikel wenden wir die hier dargestellten Inhalte auf unser Praxisbeispiel mit den Zeitreihen an.

Weiterlesen...

Eine Einführung in Denotational Design Teil II: Zeitreihen

Dieser Artikel ist der zweite einer Serie von Artikeln über Denotational Design. Im vorherigen Teil dieser Reihe hatten wir die theoretische Grundlage von Denotational Design kennen gelernt: Die denotationelle Semantik. In diesem Artikel wollen wir dieses Werkzeug nutzen, um eine konkrete Fachlichkeit zu spezifizieren.

Weiterlesen...