Wer programmiert, leidet: Die Tipparbeit beim Programmieren muss der Mensch derzeit weitgehend selber machen. (Von den trivialen Codeschnipseln mal abgesehen, die Eclipse einem auf Knopfdruck hinwirft.) Das ist nicht nur viel Arbeit, sie ist auch ziemlich fehleranfällig. Moderne Typsysteme sind schon ziemlich gut dabei, einen auf Fehler hinzuweisen, das Programm korrektfrickeln muss man aber immer noch selber. Dabei ist doch das meiste Domänenwissen schon in den Typdefinitionen und -signaturen: Program by Design heißt das Zauberwort.

Mit noch ein bisschen mehr Spezifikation könnte doch der Computer den Code schreiben? Zukunftsmusik oder Irrsinn? Eine neue Generation von Programmiersprachen wie Agda und Idris mit dazu passenden IDEs setzt den alten Traum Schritt für Schritt um: Diese Werkzeuge werden langsam zu echten Partnern bei der Entwicklung. Das Programmieren macht da nicht nur mehr Freude, sondern senkt auch die Fehlerquote dramatisch. So können sich Entwickler auf die individuellen Aspekte der Software konzentrieren, anstatt wiederkehrende Patterns immer und immer wieder umzusetzen. Sie können damit ihre Aufmerksamkeit auf die Domäne und schlussendlich auf die Interaktion mit den Anwendern richten.