Interview mit Nicole Rauch und Dr. Michael Sperber

„Agda und Idris schließen typische Fehlerquellen traditioneller Sprachen von vornherein aus“

Hartmut Schlosser

Nicole Rauch & Dr. Michael Sperber

Fehler kann man sich in der Welt der Entwickler eigentlich nicht erlauben – die Gefahr, dass das Produkt nicht rund läuft, ist viel zu groß. Doch wie kann man dem Vorbeugen? Im Interview sprechen wir mit Nicole Rauch, freiberufliche Softwareentwicklerin, und Dr. Michael Sperber, Geschäftsführer der Active Group GmbH, über die Programmiersprachen Agda und Idris, die dabei helfen sollen.

Erleben sie unsere beiden Speaker Nicole Rauch und Dr. Michael Sperber live auf der W-JAX 2017 in München! Der Vortrag mit dem Titel „Programmierpraxis übermorgen: Mensch spezifiziert, Maschine programmiert“ wird am 7. November stattfinden.

JAXenter: Ihr entwerft auf der W-JAX das Bild einer neuen Ära der Software-Programmierung: Der Mensch spezifiziert, die Maschine programmiert. Weshalb ist das überhaupt wünschenswert? Was ist das Problem mit der „alten Ära“?

Nicole Rauch & Michael Sperber: Ausgelieferte Software ist voller Fehler, und die notwendige Fehlerbehebung und Wartung haben in den letzten Jahren ihren Anteil an der Entwicklungszeit kaum reduzieren können. Bisher konnten einzelne Benutzer die aus diesen Fehlern resultierenden Probleme oft umgehen (oder hatten sich daran gewöhnt). Mit der zunehmenden Vernetzung des Internets der Dinge steigen die Häufigkeit und die Kritikalität solcher Fehler, vor allem durch Attacken.

JAXenter: Zur Realisierung dieses Zukunftsbildes stellt ihr die Programmiersprachen Agda und Idris vor. Wie unterscheiden diese sich von herkömmlichen Sprachen wie Java, C++, PHP, etc.?

Nicole Rauch & Michael Sperber: Zunächst einmal sind Agda und Idris funktionale Sprachen, die viele typische Fehlerquellen traditioneller Sprachen von vornherein ausschließen. Agda und Idris erlauben es außerdem, die Spezifikation der Software in den Code zu integrieren. Der Compiler überprüft dann, ob der Code dieser Spezifikation auch entspricht: Entwickler haben also die Möglichkeit, Korrektheitseigenschaften ihres Codes zu beweisen.

JAXenter: Wir kennen ein ähnliches Ziel bereits aus dem Bereich MDA: Model-driven Architecture. Einfach mit grafischen Sprachen wie UML die Architektur spezifizieren, den Rest erledigen Generatoren, so hieß es vor einigen Jahren. Funktioniert hat das aber nie wirklich gut. Was ist jetzt anders mit dem von euch vorgestellten Ansatz?

Nicole Rauch & Michael Sperber: Die Ansätze von Agda und Idris, die über Dependent Types funktionieren und Ansätze aus automatischen Theorembeweisern übernehmen, sind mit MDA kaum zu vergleichen. Nur weil ein Modell grafisch ist, stellt es noch keine Spezifikation dar, und viele kritische Eigenschaften von Code sind in MDA-Technologien entweder gar nicht auszudrücken oder aber die Toolchain ist nie weit genug gekommen, um ihre Korrektheit sicherzustellen. Die Agda und Idris zugrundeliegenden Techniken und Technologien sind bereits erfolgreich in einer Reihe industrieller Projekte verwendet worden, darunter CompCert und seL4.

Programmierpraxis übermorgen: Mensch spezifiziert, Maschine programmiert

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.

Jetzt Tickets für die W-JAX 2017 in München sichern!

JAXenter: Zurück zum Eingangsbild: Der Mensch spezifiziert, die Maschine programmiert. Wie nahe kommt man da in der Praxis wirklich heran mit Agda, Idris & Co. Was geht schon gut, was fehlt noch?

Nicole Rauch & Michael Sperber: Agda und Idris unterstützen Entwickler bei der systematischen Entwicklung korrekten Codes: Sie erzeugen mit Hilfe des Typsystems automatisiert Code-Teile, welche die gegebene Spezifikation nachweislich erfüllen. Das erleichtert die Konstruktion korrekten Codes ungemein und führt zu einem echten Dialog zwischen Mensch und Maschine. Dieser Ansatz ist noch recht neu. Es fehlen vor allem noch die robustere Unterstützung in mehr und gängigere IDEs sowie die Integration in industrielle Software-Ökosysteme.

JAXenter: Was ist die Kernbotschaft eurer Session, die jeder Besucher mit nach Hause nehmen sollte?

Nicole Rauch & Michael Sperber: Schreibe Eigenschaften deines Programms auf. Heute vielleicht noch als Kommentar, morgen als Code, und übermorgen als Code, dessen Korrektheit bewiesen werden kann.

Nicole Rauch ist freiberufliche Softwareentwicklerin und Softwareentwicklungscoach mit umfangreichem Hintergrund in Compilerbau und formalen Verifikationsmethoden. Neben Specification by Example, Domain-driven Design, React.js/Redux, Node.js und der Sanierung von Java-Legacy-Code-Applikationen erobern funktionale Programmiersprachen, allen voran Haskell, sich langsam aber sicher einen festen Platz in ihrem Repertoire. Neben ihrer Entwickler- und Coachingtätigkeit wirkte sie an der Ausrichtung mehrerer selbstorganisierter Konferenzen und an der Initiierung der Softwerkskammer, einer deutschsprachigen Usercommunity zum Thema Software Craftsmanship, sowie ihrer Karlsruher Regionalgruppe mit.

 

Dr. Michael Sperber ist Geschäftsführer der Active Group GmbH, die Individualsoftware ausschließlich mit funktionaler Programmierung entwickelt. Er ist international anerkannter Experte für funktionale Programmierung und wendet sie seit über zwanzig Jahren in Forschung, Lehre und industrieller Entwicklung an. Außerdem hat er zahlreiche Fachartikel und Bücher zum Thema verfasst. Michael Sperber ist Mitbegründer des Blogs funktionale-programmierung.de und Mitorganisator der Entwicklerkonferenz BOB.
Geschrieben von
Hartmut Schlosser
Hartmut Schlosser
Content-Stratege, IT-Redakteur, Storyteller – als Online-Teamlead bei S&S Media ist Hartmut Schlosser immer auf der Suche nach der Geschichte hinter der News. SEO und KPIs isst er zum Frühstück. Satt machen ihn kreative Aktionen, die den Leser bewegen. @hschlosser
Kommentare

Hinterlasse einen Kommentar

Hinterlasse den ersten Kommentar!

avatar
400
  Subscribe  
Benachrichtige mich zu: