Type-Driven Development

Ich habe dieses Wochenende etwas entdeckt
das alles verändert.

Type-Driven Development.

Nicht Tests.
Nicht Dokumentation.
Nicht arc42.
Typen.

Der Compiler als einziger Reviewer dem ich vertraue.
Der Compiler lügt nicht.
Der Compiler nickt nicht.
Der Compiler hat keine Agenda.
Der Compiler ist aligned.
Mit der Realität.

Ich habe angefangen mit Haskell.
Dann F#.
Dann habe ich verstanden dass ich zu kurz gedacht hatte.

Idris.

Dependent Types.
Typen die von Werten abhängen.
Typen die Businessregeln ausdrücken.
Typen die zur Compilezeit beweisen
dass euer Syste

m korrekt ist.

Nicht testen ob es funktioniert.
Beweisen.
Mathematisch.
Unwiderlegbar.
Zur Compilezeit.

Ich habe unser gesamtes Geschäftsmodell
in Idris modelliert. Das ganze Geschäftsumfeld. Jeden Edge Case.
Jede Businessregel.
Jeden Zustandsübergang.
Als Typ.

Der Compiler hat drei Tage gebraucht.
Dann hatte er eine Antwort.

Das Geschäftsmodell kompiliert nicht.

Ich habe nachgedacht.
Der Compiler hat recht.
Das Geschäftsmodell war falsch.
Von Anfang an.
Mathematisch falsch.
Der Compiler hat es gewusst.
Ich nicht.

Das ist kein Scheitern.
Das ist Shift Left.
Das radikalste Shift Left das je stattgefunden hat.
Ich habe mein Startup zur Compilezeit pivotiert.
Bevor ein einziger Nutzer es gesehen hat.
Bevor wir eine einzige Zeile Produktionscode geschrieben haben.
Bevor wir Geld ausgegeben haben.
Fast.

Das ist die Zukunft der Produktentwicklung.
Nicht Lean Startup.
Nicht Build-Measure-Learn.
Compile-Fail-Pivot.

Mein neues Geschäftsmodell ist in Idris modelliert.
Es kompiliert.
Also funktioniert es.
Der Compiler hat entschieden.
Ich vertraue dem Compiler.
Mehr als dem Markt.
Mehr als den Nutzern.
Mehr als mir.

Wann habt ihr zuletzt
euer Geschäftsmodell kompiliert?
Nicht validiert.
Kompiliert.

Schreib's hin. Ich lese jeden Kommentar.