Der nachfolgende Text wurden mit KI erstellt und kann Fehler enthalten. Fehler gefunden? Bei GitHub editieren
Herzlich willkommen zu einer weiteren Episode von Software-Architektur im Stream.
Diesmal mit Lars und da haben sie ja gerade eben schon die Vorenkündigung.
Also Lars, wie auch ich, werden auf dem iSAQB Software-Architecture-Forum sein.
Lars hat einen Vortrag, ich habe einen Vortrag und außerdem haben wir auch noch ein Panel, was wir gemeinsam mit einem Partner machen zum Thema Lernen und LLMs.
Und ein bisschen das Thema von heute, ich glaube ich habe etwas zu tun mit dem Thema von dem Vortrag.
Aber Lars, möchtest du dich erstmal selber vorstellen?
Ja, danke Eberhard und es freut mich mal wieder im Stream zu sein.
Mein Name ist Lars Hupel, ich arbeite bei Giesecke und Devriant und ich bin aber heute hier in meiner Funktion als Co-Kurator vom Modul Formale Methoden im iSAQB und formale Methoden sind so ein bisschen mein Herzensthema, weil ich auch in dem Bereich meine Promotion gemacht habe vor vielen Jahren.
Und ja, der Eberhard hat beschlossen, mich da mal ein bisschen dazu auszufragen und deswegen freue ich mich, da Rede und Antwort zu stehen.
Genau, ich freue mich auch auf das Thema und tatsächlich hast du drei andere Episoden.
Da gibt es zum einen die Diversity-Episode, dann gibt es eine zum Thema funktionale Programmierung und dann eine zum Thema Synchronisieren, jeweils mit anderen Leuten zusammen.
Und ich glaube, dazu kommen wir wahrscheinlich auch noch.
Ich habe das Gefühl, die CSF hat vielleicht etwas mit funktionaler Programmierung zu tun.
Könnte sein, ja.
Dann können wir loslegen mit der Frage, was sind denn überhaupt formale Methoden?
Und ich glaube, du hattest da so ein bisschen Grafik mitgebracht.
Genau, also formale Methoden, ich glaube manche haben davon schon mal gehört, dass das irgendwas mit Beweisen von Dingen zu tun hat.
Aber es ist eigentlich ein ganzer Bündel von verschiedenen Maßnahmen, die man machen kann, um grob gesagt die Korrektheit von Software zu verbessern, sage ich mal ganz allgemein.
Und ich habe mal hier ein Diagramm mitgebracht.
Das ist auch die einzige Folie, die ich zeigen will heute.
Also es wird jetzt keine PowerPoint-Präsentation hier.
Und zwar habe ich mal hier verschiedene formale Methoden zusammengetragen.
Und zwar haben wir eine X-Achse und eine Y-Achse.
Die X-Achse, die geht so ein bisschen von Spezifikation zu Implementation.
Also je weiter rechts wir sind, desto mehr können wir abdecken.
Also wir haben bestimmte formale Methoden, die beziehen sich rein auf eine Spezifikation der Software.
Das heißt, da reden wir gar nicht über Code oder sowas, sondern über so ein Modell einfach.
Und ganz rechts haben wir dann etwas, was tatsächlich sich auf die konkrete Implementierung, also Java, Go, Swift, was auch immer bezieht.
Das wäre also die X-Achse.
Das habe ich jetzt einfach mal Rigor genannt.
Also wie rigoros sind die?
Und je weiter wir nach oben gehen, desto mehr Zusicherungen bekommen wir.
Und eben hier sind ein paar ganz verschiedene Beispiele.
Was oftmals gemeint ist, wenn man mit formalen Methoden redet, ist rechts oben Model Checking und Theorembeweiser.
Hat vielleicht der eine oder die andere schon mal was davon gehört.
Also ein Theorembeweiser, das ist ein Tool, mit dem man tatsächlich mathematische Aussagen, also Definitionen, Satz, Beweis, wie man das so aus dem Mathebuch kennt, wirklich führen kann und dann gegenüber der Software rechtfertigen muss, dass das, was man gemacht hat, auch korrekt ist.
Dann gibt es noch so einen Punkt, den ich immer in die Mitte gepackt habe.
Flowcharts, also Flowcharts, wer sich irgendwie an UML erinnert.
Die haben auch irgendwie eine feste Syntax und Semantik.
Und dann kann ich erst mal irgendwie abstrakt hinschreiten, was meine Software eigentlich machen soll.
Und ich kann mich dann immer weiter nach links bewegen in den Spezifikationsbereich.
Da hätten wir zum Beispiel erststufige Logik.
Damit kann ich zum Beispiel hinschreiben, wie sich bestimmte Zustände verhalten.
Auch State Machines wäre sowas.
Ich könnte zum Beispiel aufmalen, durch welche Zustände sich meine Software bewegen kann.
Und vielleicht habe ich auch mehrere Threads, die verschiedene Zustände haben.
Und das Gängigste allerdings, was wahrscheinlich die allermeisten benutzt haben, ist links oben nämlich ein Typsystem.
Ein Typsystem ist auch eine bestimmte, hart von der Formalmethode.
Da muss ich gegenüber dem Computer rechtfertigen, dass das, was ich gemacht habe, auch einigermaßen richtig ist.
Ein Typsystem stellt nicht sicher, dass meine Implementation wirklich korrekt ist.
Aber es stellt zumindest mal sicher, dass ich jetzt nicht irgendwie, keine Ahnung, ok, manche Sprachen können das nicht, aber in vielen Sprachen kann ich zum Beispiel Nullpointer ausschließen damit.
In Java ist das nicht der Fall.
Aber ich kann auch in Java zum Beispiel bestimmte Sachen ausschließen.
Dann kriege ich in Java im Regelfall keinen Segmentation-Fault, weil ich irgendwie auf einen Nullpointer zugegriffen habe.
Also meistens kann ich das dann irgendwie sauber abfangen.
Also das ist so ein bisschen der Bereich, in dem wir uns bewegen.
Und um das nochmal zusammenzufassen, es gibt also ein Bündel an Maßnahmen, die sich entweder auf Spezifikations- oder auf Implementationsebene abspielen, mit denen ich bestimmte Eigenschaften über mein Programm sicherstellen kann.
Dass es eben korrekt ist, oder dass es bestimmte Zustände nicht einnehmen kann, oder dass es bestimmte Zeit dauert, nur um eine bestimmte Anfrage abzuweiten.
Alles diese Themen kann ich damit eben abdecken.
Also sozusagen Nachfragen an der Stelle.
Bei dem Typsystem wäre mir jetzt als erstes eingefallen, diese Geschichte mit, wenn ich halt eine Funktion habe, die hat einen String erwartet, und ich gebe dem einen Integer rein, dann sagt er mir, das System geht halt nicht.
Das heißt, mindestens bezüglich Typen ist das halt korrekt.
Und das ist halt ja etwas, was ich statisch zur Compile-Zeit oder dynamisch zur Laufzeit hinbekomme.
Und das ist jetzt das Erste, was mir eingefallen war, weil du sprachst über so etwas wie, dass Kanalpointer da ist.
Richtig.
Da hast du einen wichtigen Begriff genannt.
Das meiste handelt sich wirklich um statische Analysen.
Das heißt, alle diese Sachen, die ich hier auf der Folie habe, sind tendenziell überwiegend ohne Runtime.
Das heißt, das sind alles Sachen, die ich mache, indem ich mir den Code anschaue.
Und das führt eben dazu, dass ich ahead of time, also ohne dass ich die konkreten Inputs schon kenne, dass ich bestimmte Aussagen treffen kann.
Und man kann dann eben so Aussagen treffen wie, für alle Inputs von 0 bis 1000 gilt eben das und das.
Und das ist eben etwas, was wir mit Testing im Regelfall nicht machen.
Im Testing greifen wir uns im Regelfall bestimmte Fälle aus, von denen wir denken, dass sie irgendwie gängig sind oder dass sie Ausnahmefälle sind.
Aber ich kann eben keine allgemeingültigen Eigenschaften durch Testing beweisen.
Da gibt es ja diesen berühmten Spruch, also ich kann durch Testen nur die Anwesenheit von Fehlern zeigen, aber eben nicht die Abwesenheit von Fehlern.
Und bei formalen Methoden sagt man, wir wollen eben versuchen, den gesamten Zustandsraum oder zumindest zu einem signifikanten Teil das irgendwie anzudecken und uns abstrakt Gedanken zu machen, was kann denn alles passieren und das dann irgendwie berücksichtigen.
Was dann bedeutet, dass diesbezüglich statische typisierte Sprachen sozusagen die bessere Wahl sind?
Weil sonst würde ich ja erst vor der Laufzeit herausbekommen, dass ich einen Typfehler habe.
Genau, also es gibt auch formale Methoden, die ich auf dynamisch getypten Sprachen laufen lassen kann.
Aber das macht es sehr, sehr schwer, weil ich dann ständig erstmal beweisen muss, dass ich jetzt hier nicht irgendwie einen String in den Int konvertiert habe.
Und auch so Sprachen wie C sind ein bisschen schwierig, weil das Typsystem sehr, sehr lax ist.
Also da können ganz viele Dinge passieren.
Und das andere Ende der Fahnenstange wäre dann sowas wie Rust oder Haskell, wo ich halt sehr, sehr viele Sachen im Typsystem schon mal abdecken kann.
Aber ganz wichtig ist, wenn euch jemand Typsysteme verkauft als das absolute Korrektheitsmittel, dann ist das vielleicht nicht komplett verkehrt, aber das ist auf jeden Fall nur die halbe Wahrheit.
Also ein Typsystem ist cool, aber wenn ich dann wirklich inhaltliche Implementationen, Aussagen treffen will, dann reicht das vielleicht nicht.
Genau, und dann warst du auf First Order Logic eingegangen und hattest dann aber als Beispiel sofort eine State Machine genannt.
Also eine State Machine wäre ja sowas, dass ich sage, eine Bestellung ist halt, was sie nicht, also nehme ich jetzt jedenfalls an, das wäre das, was mir einfällt.
Eine Bestellung ist halt bestellt, dann ist sie halt irgendwie storniert.
Und dann kann sie irgendwie zugestellt sein.
Sie kann nur zugestellt sein, wenn sie nicht storniert ist.
Solche Geschichten hätte ich jetzt erwartet, so mit Zustandsübergängen.
Genau, also ich würde dann zum Beispiel sagen, das kann man sich ganz einfach vorstellen.
Ich stelle mich an ein Whiteboard und male erst mal auf, was ich alles für Zustände habe und was es überhaupt für Übergänge geben kann.
Und dann stelle ich zum Beispiel fest, Moment mal, wenn jetzt die Order in einem Zustand pending ist und gleichzeitig ich irgendein Event im Lager habe, dann könnte es sein, dass ich die Bestellung verschicke, obwohl die Zahlung gar nicht eingegangen ist.
Also das sind eben solche Fälle, die ich dann versuche abzudecken.
Und das kann man beispielsweise durch State Machines machen, aber es gibt auch noch andere Mechanismen, wie man das machen kann, zum Beispiel mit einem Flowchart.
Oder ich versuche irgendwie Eigenschaften über die Software mit Prädikatenlogik hinzuschreiben.
Also erststufige Logik und Prädikatenlogik ist das Gleiche.
Und dann könnte ich zum Beispiel sagen, ich modelliere mir jetzt irgendwie meine Bestellungen als Menge von Dingen und dann habe ich da irgendwie ein Prädikat darauf, ob die jetzt abgearbeitet sind oder nicht.
Also da kann man sich mehrere beliebige Sachen ausdenken in diesen Fällen, wie man das jetzt genau modelliert.
Und hattest du ja gesagt, dass ich beispielsweise für diese State Machine hin war mit verschiedenen Zuständen und Übergängen dazwischen und dann irgendwie sozusagen darüber nachdenken, dass eben bestimmte Dinge da passieren können.
Hört sich jetzt nicht so super formal an, in dem Sinne, dass ich einen Ansatz habe, der jetzt sagt, ja, das System ist korrekt, sondern hört sich für mich an, wie ich mal das mal und ich mache es mir irgendwie selbst klar.
Ist das tatsächlich eine formale Methode?
Ja, da kommen wir jetzt schon ganz in die Definitionssachen rein.
Also wenn man jetzt jemanden fragt, der Theorembeweiser benutzt, also der ganz rechts oben in der Ecke ist, wie ich zum Beispiel in meiner Forschungsarbeit gemacht habe, dann würde ich natürlich sagen, ja, Moment mal, damit kann ich jetzt irgendwie noch nicht so wahnsinnig viel beweisen über meine Software.
Das ist jetzt dann irgendwie gar nicht implementierungsnah, das ist jetzt nur ein Modell.
Und das stimmt natürlich auch zu einem gewissen Grad.
Trotzdem ist es so, dass wenn ich überhaupt erstmal nachdenke, welche Zustände meine Software überhaupt mal einnehmen kann.
Also allein die Tatsache, dass ich jetzt darüber nachgedacht habe und das mal aufgeschrieben habe, allein dadurch lerne ich schon sehr viel darüber, was ich eigentlich machen will.
Das heißt, allein der Akt des Modellierens, das könnte ich theoretisch sogar auch auf Englisch oder auf Deutsch machen, das könnte ich auch Prosa schreiben und ich sage, jetzt diskutiere ich jetzt mal der Reihe nach durch, was ist denn jetzt eigentlich die Definition von einer Bestellung?
Also was sind denn jetzt eigentlich die Komponenten, die in eine Bestellung reingehören und was ist denn jetzt der Wertebereich davon?
Und dann kommt man vielleicht irgendwie auf die Frage, ja Moment mal, was ist eigentlich jetzt, wenn irgendwie der Umsatzsteuersatz hier irgendwie nicht definiert ist?
Und dann komme ich irgendwie so ins Denken.
Und allein das hilft schon mal.
Aber das würde man natürlich jetzt in der reinen Lehre nicht als formale Methode bezeichnen, weil formale Methode heißt eigentlich, dass ich irgendeinen Formalismus benutze, der eine bestimmte definierte Syntaxe und Semantik hat und ich dann bestimmte Aussagen dann auch wirklich treffen kann.
Also bei Zustandsmaschinen kann ich zum Beispiel sowas testen wie Nichterreichbarkeit.
Gibt es irgendwelche Zustände, die irgendwie schädlich wären?
Und dann will ich gucken, dass ich die auch wirklich nicht erreichen kann.
Also irgendwie, keine Ahnung, im Auto wäre zum Beispiel ein Zustand sehr schädlich, dass ich die Bremse nicht mehr betätigen kann.
Gibt es schon Fälle, also zum Beispiel, wenn ich das Auto ausgeschaltet habe, dann tut das wahrscheinlich nichts, wenn ich auf die Bremse drücke.
Aber wenn das Auto fährt, sollte ich diesen Zustand vielleicht nicht erreichen können.
Das wäre irgendwie blöd.
Okay, was also bedeutet, dass ein Typechecker dann tatsächlich sozusagen eine richtige formale Methode ist, weil das Ding sagt mir ja typmäßig korrekt oder eben nicht korrekt.
Du hattest jetzt gesagt, es gibt sozusagen eher informelle Methoden, wo ich halt irgendwie drüber nachdenke.
Genau, das war auch ein bisschen Sinn, dieser Folie zu zeigen, dass es da wirklich ein Spektrum gibt.
Und es ist halt immer so eine Diskussion von Leuten, die vielleicht schon mal davon gehört haben, aber das noch nie benutzt haben, die sagen, oh meine Güte, das ist ja irgendwie so furchtbar aufwendig, aber muss es auch nicht sein.
Jetzt hattest du schon mehrfach sozusagen als ein sehr mächtiges Werkzeug diese Theorienprover erwähnt.
Was genau ist das?
Wie würde ich das benutzen?
Du hast es ja offensichtlich benutzt, also wofür benutze ich das dann?
Genau, also ein Theorembeweiser, das ist mehr oder weniger ein, wie kann man sich das vorstellen, also man muss irgendwie dem Computer was erklären und dann sagt der Computer, glaube ich dir oder glaube ich dir nicht.
Und das hat dann im Prinzip die Struktur von der mathematischen Theorie.
Also ich versuche mal, ein konkretes Beispiel zu machen.
Stellen wir uns mal Sortierfunktionen vor.
Sortierfunktionen sind relativ klar, was die machen sollen.
Die nehmen irgendwie ein Array oder eine Liste oder was auch immer für eine Datenstruktur und vielleicht noch irgendwie eine Comparison-Funktion, wo ich sagen kann, das Element ist kleiner als das andere.
Und dann habe ich auch einen ziemlich klaren Kontrakt.
Also ich gebe irgendwie ein nicht leeres Array rein und bekomme ein nicht leeres Array raus.
Gleiche Größe vom Output wie vom Input.
Es müssen die gleichen Elemente drin sein und sie müssen sortiert sein.
Also das ist irgendwie relativ klar, was eine Sortierfunktion machen soll.
Und dann kann ich eben in dem Theorembeweiser diese Sortierungsfunktion implementieren.
Jetzt gibt es von diesen Theorembeweisern auch viele verschiedene.
Ich nehme mal als Beispiel Isabelle, weil mit Isabelle kenne ich mich am besten aus.
Das ist halt einfach das System, was wir benutzt haben in der Uni.
Isabelle ist im Prinzip eine funktionale Programmiersprache.
Das heißt, man stellt sich mal vor, man nimmt eine Sortierfunktion, die man in Scala geschrieben hat oder in Haskell.
Dann kann man die relativ eins zu eins nach Isabelle übersetzen.
Also man tippt dann halt auch einfach Funktionsdefinitionen, Datentyp-Definitionen, kann dann rekursiv irgendwelche Dinge tun.
Dann hat man erst mal nur die Funktion.
Die kann man auch ausführen, aber dann hat man noch nichts bewiesen.
Und dann kann man eben in Isabelle hinschreiben, Theorem, Doppelpunkt, unter der Annahme so und so.
Dann kommt bei der Sortierfunktion immer das und das raus.
Dann kann ich zum Beispiel schreiben, der Output von meiner Sortierfunktion ist immer sortiert.
Und dann sagt Isabelle, ja cool, du musst das jetzt beweisen.
Und dann sage ich Isabelle, okay, ich möchte das jetzt beweisen.
Zum Beispiel per Fallunterscheidung, per Negation, also per Widerspruch oder per Induktion oder per was auch immer.
Also ich kann dann sagen, ich mache diese Beweismethode.
Und dann sagt Isabelle, cool, du machst das per Fallunterscheidung.
Dann gib mir doch mal den Fall, was passiert, wenn die Leereliste reinkommt.
Dann gib mir doch mal den Fall, was passiert, wenn eine Nicht-Leereliste reinkommt.
Also im Prinzip kriege ich dann so das Aufgefaltete rein.
Und ich kann dann so immer reinzoomen.
Und das muss ich dann als User machen.
Also wenn ich dann Isabelle bediene, muss ich dann immer erklären, wie jeder Teilschritt funktioniert.
Und irgendwann bin ich in einer Granularität angekommen, wo das System sagt, okay, das glaube ich dir.
Das kann ich nachvollziehen.
Also ich habe jetzt glaube ich dir gesagt.
Das ist natürlich nichts mit Glauben.
Das ist natürlich genau definiert, was es mir glaubt und was nicht.
Es gibt dann einen Kernel.
Und dieser Kernel überprüft jeden einzelnen Schritt.
Das heißt, am Ende des Tages habe ich dann irgendwie so einen Beweis.
Und dann geht der Kernel das Schritt für Schritt durch und sagt, passt, passt, passt oder passt nicht.
Und wenn er sagt, passt nicht und ich Glück habe, kann er mir sogar ein Gegenbeispiel angeben.
Dann würde er zum Beispiel sagen, also wenn du jetzt hier eine Liste von fünf Integers hast und der erste Integer ist eine 4 und der dritte Integer ist eine 8, dann hast du irgendwie eine Optimierung gemacht und die funktioniert dann nicht mehr.
Also das können die Tools oftmals auch machen.
Und ich beschreibe das formal, was da passiert, nehme ich an.
Weil du sagst, ich erkläre das.
Das ist dann etwas, was ich formal mache, was irgendwie bedeutet, dass ich das Programm dann noch weiter ergänze durch solche zusätzlichen Informationen.
Das ist jetzt ein interessanter Punkt.
Es gibt Systeme, in denen ich das Programm tatsächlich ergänzen muss.
Also da kann ich mir zum Beispiel, stellen wir uns mal vor, ich schreibe ein Java Programm, dann klatsche ich einfach noch ein paar Annotationen ran.
Dann würde ich sagen, also hier bei diesem while loop muss ich jetzt noch annotieren, warum die jetzt terminiert.
Hier bei diesem Rekursionsaufruf muss ich noch eine Annotation dran machen, wie sich das Argument verhält, wie auch immer.
Das ist nicht das, was ich in Isabelle mache.
In Isabelle ist das sauber getrennt.
Da habe ich auf der einen Seite die Implementierung und dann habe ich noch eine eigene Sprache, die nennt sich Isar.
Das ist eine Abkürzung, steht für Intelligent Semi, nein, Intelligible Semi Automated Reasoning.
Also es ist so wie lesbar, intelligible.
Ich kann das also wie so ein Mathebuch lesen.
Da steht dann so proof by, have, then have, then have, also assume, bla bla bla.
Das ist wirklich sowieso Englisch, schließt sich das.
Aber es hat natürlich eine sehr strukturierte Syntax.
Und Semi Automatic heißt, dass das System teilweise versucht, Schritte auch zu automatisieren.
Also der versucht jetzt nicht von mir, der will nicht von mir, dass ich x plus y gleich y plus x beweise.
Also solche einfachen Schritte kann der selber machen.
Der will im Prinzip von mir, dass ich die Struktur runterbreche in kleine verdauliche Happchen und dann das System jeden Schritt einzeln prüfen kann.
Und das ist eben in Isabelle sauber getrennt.
Es gibt eben, wie gesagt, andere Systeme, wo ich das im Code mit drin habe, was Vor- und Nachteile hat.
Also der Vorteil ist, dass ich es halt direkt im Code habe.
Der Nachteil ist, dass ich es direkt im Code habe.
Also kann man sich jetzt überlegen, was schöner ist.
Okay, wie soll ich sagen?
Also ich glaube jetzt sofort, dass das halt ein Thema ist, was ich halt, du hast jetzt so Tieralgorithmen genannt, was ich da vielleicht irgendwie benutzen will, weil ich halt irgendwie absichern will, dass ein Standard-Library nun wirklich wasserdicht ist.
Mir fallen auch insbesondere so Kryptografie-Geschichten ein, wo man sich halt darauf verlässt, dass die halt richtig implementiert sind und dass da halt irgendwie keine Fehler drin sind, die dazu führen, dass ich es halt irgendwie knacken kann.
Ich muss jetzt gestehen, also ich mache das jetzt mit der Software-Architektur, mit Software-Entwicklung seit gut 30 Jahren und ich habe tatsächlich irgendwie im Studium natürlich theoretische Informatik gehabt.
Das heißt, ich habe so ein bisschen Ahnung, worüber du diskutierst.
Aber in meinem professionellen Leben und gegen Geld ist mir das irgendwie noch nie ernsthaft begegnet, weil ich sozusagen nicht typisch normale, in Anführungsstrichen, IT-Systeme baue.
Warum?
Beziehungsweise habe ich da irgendwas vergessen oder hätte ich das irgendwo nutzen sollen?
Oder was ist da der Punkt?
Wobei man muss natürlich einschränken.
Eine State-Machine habe ich schon mal aufgemalt oder darüber nachgedacht, dass das irgendwie schief sein kann.
Das ist, glaube ich, relativ klar.
Vielleicht ist das auch schon Ergebnis von der Episode.
Aber so etwas wie einen Theorienprover habe ich ehrlich gesagt noch nie vermisst, wäre mein Gefühl.
Also es ist natürlich schon so, je höher und je weiter nach rechts ich in diesen Diagramm komme, desto teurer wird es.
Es gibt ja schon Leute, die finden Typ-Systeme nicht gut, also in Rust ist das ja immer so ein Meme, das man irgendwie länger braucht, um dann den Typ-Checker zufriedenzustellen, als den eigentlichen Code zu schreiben.
Und je weiter man nach oben und rechts kommt, also so etwas wie Isabelle zu benutzen, ist halt sehr aufwendig.
Warum?
Weil ich sehr viel mehr Aufwand in die Implementierung stecken muss.
Es gibt da immer so verschiedene Faustformeln, die da so rumgeistern.
Eine Faustformel ist, dass auf eine Zeile Code so zehn Zeilen Verifikation kommen.
Zehn Zeilen Isabelle Code beispielsweise.
Manche Schätzungen sind noch pessimistischer.
Und das führt natürlich einfach knallhart dazu, dass die Entwicklung von Software deutlich teurer wird.
Und ich sage jetzt mal ganz flapsig, wenn ich jetzt irgendwie eine mobile App baue und ich irgendwie beweisen müsste, dass die nie crashen kann, dann ist das vielleicht der Return of Investment nicht ganz so klar.
Aber es gibt natürlich schon Branchen, in denen ein Crash nicht akzeptabel ist und dann einfach noch viel teurer wäre, als die formalen Methoden zu machen.
Und in diesen Branchen werden dann eben formale Methoden eingesetzt.
Und das sind eben Branchen wie zum Beispiel Healthcare, Defense, Aviation.
Das sind eben so diese drei Haupt-User, würde ich mal fast sagen, ohne jetzt die Statistiken zu kennen.
Aber das ist oftmals Software, wo ich mir eben nicht erlauben kann, dass irgendwie ein Fehler drin ist.
Und weil ich gerade von der App geredet habe.
Also klar, wenn die App crasht, ist es vielleicht nicht so schlimm.
Also ich habe jetzt zum Beispiel meine Banking-App und dann schaue ich meinen Kontoauszug an.
Wenn die crasht, okay, geschenkt.
Wenn aber durch den Crash eine Überweisung doppelt gemacht würde, dann wäre das vielleicht nicht so cool.
Also es ist immer so eine Abwägungsgeschichte.
Wann rechtfertige ich das?
Und deswegen muss man halt auch manchmal ganz klar wirtschaftlich denken und sagen, okay, für diesen Teil von meiner Software ist es vielleicht einfach gar nicht relevant.
I am the Slime bemerkte nur, dass du eine Scala-Legende bist.
Ja, danke.
Ich war tatsächlich sehr viel im Scala-Umfeld unterwegs und habe da auch formale Methoden mal gemacht.
Ich war mal für ein paar Monate in Lausanne in der EPFL und die haben dort ein Tool entwickelt, mit dem man Scala-Code korrekt beweisen kann.
Also ich habe auch mal versucht, diese beiden Workstreams irgendwie zusammenzubringen.
Okay, genau.
Ah, und dann hat Herr Erder sich auch gleich noch eine Frage gestellt, haben die Theorienprover eigentlich das Problem, dass auch mit Tests aufkommen kann?
Woher weiß ich, dass mein Proof kein Fehler hat?
Da kann ich eine schöne Anekdote dazu sagen.
Es gab bei uns am Lehrstuhl immer so das Motto, Beweis durch korrekte Definitionen.
Was heißt das?
Je nachdem, wie ich meine Definitionen mache, also ob ich die Sortierfunktionen so definiere oder anders definiere oder meine Korrektheits-Eigenschaften so definiere oder anders definiere, kann es sein, dass der Beweis sehr einfach oder sehr schwierig wird.
Man kennt das ja manchmal, man versucht sehr kompliziert, etwas zu implementieren und stellt dann erst zwei Tage später fest, das hätte ich ja viel einfacher machen können mit dem gleichen Effekt.
So etwas kann eben bei formalen Beweisen auch passieren, dass die Definitionen einfach sehr wichtig sind, also wirklich tragende Säulen sind.
Dann habe ich manchmal zwei Definitionen, die sehen irgendwie fast ähnlich aus, aber sind dann subtil anders.
Konkretes Beispiel, die, die Mathe studiert haben, müssen jetzt mal kurz die Ohren zuhalten.
In Isabelle kann ich durch Null dividieren.
Also ich kann durch Null dividieren und dann bekomme ich Null raus.
Das ist mathematisch unproblematisch, wenn man immer die richtigen Vorbedingungen hat.
Ich kann dann dadurch nicht plötzlich irgendeinen Widerspruch herleiten in der Mathematik.
Das denkt man dann immer.
Aber das ist für viele Leute erst mal ungewohnt.
Dann denken die so, warum kann ich denn das jetzt beweisen?
Das ist doch irgendwie Division durch Null.
Es ist natürlich so strukturiert, dass man anders keine anderen Probleme kriegt.
Also wie gesagt, ich kann jetzt keinen Widerspruch herleiten.
Aber das kann manchmal passieren, dass ich Definitionen so geschrieben habe, dass sie irgendwie unintuitiv sind oder dass sie irgendwie nicht das beweisen, was ich gedacht habe, dass es beweist.
Das kann manchmal vorkommen und da hilft dann halt nur, wenn man nochmal einen anderen Blick drauf wirft.
Also einfach mal nochmal eine Kollegin oder so fragt, findest du, dass das irgendwie richtig aussieht?
Ausschließen kann man solche Sachen nicht.
Was man schon einigermaßen ausschließen kann, ist, dass das System Sachen akzeptiert, die einfach falsch sind.
Die Architektur von diesen Theorembeweisern ist so gebaut, dass ich eben diesen Kernel habe.
Der Kernel ist relativ klein, also dass praktisch der Kernel einen Bug hat, der dafür sorgt, dass mein Beweis durchläuft, obwohl man gar nicht durchlaufen sollte.
Das ist extrem selten.
Das kommt alle zehn Jahre vielleicht einmal vor.
Aber die meisten Fehler entstehen dadurch, dass man einfach Dinge beweist, die was anderes sind, als man geglaubt hat, was man bewiesen hat.
Ich weiß gar nicht, wo ich das aufgeschnappt habe, dass mathematische Beweise eigentlich nur ein soziales System sind.
Da müssen Leute drüber gucken.
Erst wenn genügend Leute drüber geguckt haben, dann ist es eben ein offiziell richtiger Beweis.
Insbesondere bei diesen nicht trivialen Beweisen, die überall Seiten und Seiten gehen.
Das kann ich durch Theorembeweiser ein Stück weit noch unterstützen, indem ich sage, okay, wenigstens sind die logischen Schlussfolgerungsschritte korrekt.
Aber wenn jetzt jemand reingeht und sagt, ich definiere irgendwie meine abstruse Mengen, Mannichfaltigkeit, Faserbündel, Gedöns, irgendwie anders, als alle anderen das definiert haben, dann habe ich halt irgendwie nicht gekonnt dabei.
Ah, da muss ich auch wieder Jein sagen, weil Isabelle hat das nicht.
Aber es gibt Konkurrenztools, zum Beispiel Lean, bei denen ist es so, da gibt es eine richtige Implementierung und dann gibt es noch eine zweite Implementierung, die praktisch in Reihenraum nochmal neu geschrieben worden ist, nur von diesem Proofkörner.
Und dann kann man den Beweis durch das Hauptsystem durchnudeln lassen, dann kommt da irgendwie so ein Trace raus, dann kann man diesen Trace nochmal durch das Zweitsystem durchnudeln lassen und dann hat man einen Proofprober.
Und dann kann man sich die Frage stellen, gibt es einen Proofproberprober?
Also irgendwie muss man das dann auch mal aufführen.
Aber es gibt zumindest Systeme, die haben diesen Ansatz, dass man unabhängig nochmal eine sekundäre Implementierung einer anderen Programmiersprache hat, um eben wirklich diese Kernelbugs möglichst ausschließen zu können.
Es gab vor einigem, also wir haben ja bei Software Direktur im Stream dieses Formular auf der Webseite, wo man nämlich Fragen stellen kann.
Und da gab es vorher, ehrlich gesagt, ziemlich lange Zeit eine Frage, die jetzt in diese Episode ganz gut reinpasst.
Und zwar hat die Person gesagt, angesichts all dieser Remote Code Exploits, und da gibt es irgendwie von diesem CVE, wo die ganzen Security-Probleme drin sind, war dann eine Query reingebaut, mit eben den ganzen Remote Code Exploits, wo ich also einem System sage, ich führe bitte diesen Code aus und der führt es dann eben auf dem Server halt aus, was offensichtlich ein Security-Problem ist.
Und da war dann die Frage, also wenn das halt so ist, wenn es halt all diese Remote Code Exploits gibt, warum ist dann formale Verifikation von Code-Libraries nicht längst Standard in der Software-Architektur?
Ja, das ist eine gute Frage, eine sehr gute Frage.
Ich habe zwei Antworten darauf.
Die erste Antwort ist, das ist eines der Gründe, warum Rust so populär wird für systemnahe Programmierung, weil in Rust eben mit dem Typsystem, also da sind wir wieder hier links oben in den Diagrammen, im Typsystem schon sehr viele Sachen ausschließen kann.
Beispielsweise kann ich jetzt in Rust nur sehr, sehr schwer hinkriegen, dass ich irgendwie über Speicher darüber hinweg schreibe oder dass ich irgendwie ungültige Speicherzugriffe habe oder eben sowas wie Speicher, der eigentlich X repräsentiert, dann als Y interpretiere.
Das sind halt Sachen, die können in C sehr schnell passieren und in Rust halt, also Rust ist jetzt auch nicht bug-frei, aber es können halt solche Sachen in Rust schwieriger zu exploiten.
Das ist also die erste Antwort.
Die zweite Antwort ist, es gibt Bibliotheken, auch die, die in C geschrieben sind, wo genau diese Dinge verifiziert werden, in Isabelle beispielsweise und in anderen Tools.
Ich habe mal zwei Beispiele mitgebracht, also ein Beispiel wäre ein Mikrokörner von einem Betriebssystem.
Da rede ich jetzt wieder von einer anderen Art von Körner.
Also ein Betriebssystem Körner, da gibt es ein Betriebssystem, das heißt L4 und das ist so eine Mikrokörner-Architektur, die wird viel in Embedded Systems benutzt und da hat eine Forschungsgruppe in Australien oder eigentlich sind das mehrere Gruppen gewesen, die haben das komplett verifiziert und haben dann zum Beispiel eben bewiesen, dass solche Sachen wie eine Code Execution Vulnerability oder irgendwelche Null-Points oder was auch immer eben nicht passieren können.
Das war aber extrem aufwendig, da hat man diese Schätzung, dass das irgendwie zehnmal länger dauert oder so, weil C eben wirklich schwierig zu verifizieren ist und das ist tatsächlich ein Tool, was eingesetzt wird, also das hat praktische Anwendungsfälle, damit hat man aber sozusagen im normalen Software-Engineering vielleicht nichts zu tun.
Ich glaube, wir sollten Erwähnen nicht Mikrokörner als Mikrokörner, weil der kann nur Task-Switching oder sowas nicht, also ganz wenig Funktionalität.
Genau, ihr macht halt das typische Speicherallokation und Verwaltung, Prozesse starten und managen und Inter-Prozess-Kommunikation und dann kann man da auch noch Treiber reinladen, aber die sind eben als eigene Anwendung gemacht und dann habe ich eben schon mal sichergestellt, dass zumindest wenn eine Applikation crasht, dass die anderen Applikationen nicht mitgenommen werden oder dass die sich nicht gegenseitig in ihren Speicher reinschreiben oder solche Sachen.
Das zweite Beispiel, wo mal jemand ein richtig großes Projekt gemacht hat und ein großes Stück Software verifiziert hat, das ist das CompSeer-Projekt oder CompCert, je nachdem, ob man es Französisch oder Englisch ausspricht.
Das ist in einem anderen Theorembeweiser gemacht, also das SEL4 wurde in Isabelle gemacht, das andere wurde in Rock gemacht und da hat man einen C-Compiler verifiziert, also praktisch bewiesen, dass in einem bestimmten C-Compiler, also man hat den dann implementiert für das Projekt, hat man keinen bestehenden genommen, hat einen neuen gebaut, dass also der Compiler keine Bugs baut.
Also wenn man ein Programm reinschiebt, ist das, was rausgekommen ist, als Kompilat immer noch das Gleiche.
Kann natürlich sein, dass vorher schon Bugs drin waren im Programm, aber der Compiler füllt zumindest keine neuen Bugs ein und dann kann man so spaßige Sachen beweisen, dass irgendwelche Compiler-Optimierungen korrekt sind, weil in GCC ist halt oft mal so ein Ding, dass der abstruse Optimierung implementiert und die sind dann halt vielleicht falsch oder funktionieren nur in 2% der Fälle falsch oder sowas.
Und das ist dann halt schon etwas, was in der Industrie auch benutzt wird, also halt vielleicht nicht in der Industrie, in der wir uns hauptsächlich bewegen.
Da kommt dann halt wieder die Kostenfrage rein, aber ich würde schon behaupten, es gibt Firmen, es gibt Leute, die machen sowas und wir sehen es vielleicht nicht unbedingt.
Du hattest es ja vorhin gesagt, Aviation oder so, Flugzeuge, solche Sachen.
Aber es gibt auch so, der Mike Sperber benutzt, der ist ja auch Co-Kurator von dem FM-Modul im Isaak-UB, der benutzt immer das Beispiel mit dem Tacho in Autos.
Also Tachos in Autos, die müssen auch bestimmte Auflagen erfüllen, dass sie also nicht zu schnell, nicht zu wenig anzeigen und deswegen, da werden dann halt auch bestimmte formale Methoden genutzt, vielleicht nicht Theorembeweiser, aber halt andere Methoden, um sowas sicherzustellen, dass man einfach standardkonform ist.
Also es gibt bestimmte Standards, Regulatorik und da muss man eben beweisen, auf einem bestimmten Level, dass man diese Standards erfüllt und da kann man nicht einfach nur ein Dokument abgeben und dann muss man halt wirklich ein rigoroses Argument liefern.
Das sind aber glücklicherweise, sage ich mal fast, Sachen, mit denen wir uns nicht immer nur zuständig überall behängen müssen.
Das ist halt dann schon für sehr spezielle Anwendungsfälle.
Also letztendlich haben wir ein wirtschaftliches Thema, nicht, wie du gesagt hast.
Das heißt, für die meisten Sachen ist es eben wahrscheinlich akzeptabel, mit dem Level an Fehlern einzuleben.
Es gibt eine Frage von HappyTree5812 und die Frage ist, ist nicht am Ende wie immer das Problem, dass der State Space zum Beweisen von nicht trivialen Problemen einfach zu groß ist, also dass diese Dinger zu viele Zustände haben?
Kurze Antwort, ja, das ist ein Problem.
Wir können mit dem Problem umgehen, indem wir an bestimmten Stellen uns dafür entscheiden, das zu vereinfachen.
Also konkret das Beispiel von von uns im Projekt.
Wir haben natürlich eine Software, die redet mit einer Datenbank, wie fast jeder und wir könnten jetzt entweder das Postgres mit einbeziehen in die kündigen Korrektheitsbeweis und dann müsste man irgendwie die gesamte formale Semantik von Postgres irgendwie mit aufschreiben und die Tabellen können in 25 Zuständen sein und der Index kann irgendwie ein A-Index, ein B-Index oder ein Wasserfrimmer-Index sein und ich kann irgendwie Triggers und sonst was haben.
Das macht es natürlich viel zu kompliziert.
Deswegen machen wir einen Trick, den nennen wir Relationale Algebra.
Hat man vielleicht im Informatikstudium, wer das studiert, hat schon mal gehört.
Also wir können SQL-Datenbank als Relationale Algebra modellieren.
Das heißt, wir haben einfach eine Liste von Tuplen in irgendeiner Tabelle drin und dann modellieren wir das alles so und dann sparen wir uns schon mal einen Haufen Gedöns davon.
Dann können wir uns auf das eigentlich Wichtige konzentrieren.
Damit können wir dann immer noch interessante Sachen beweisen.
Also wir arbeiten dann halt eben auf einem Modell und das führt eben dazu, dass ich möglicherweise in der Implementierung irgendwas habe, was ich nicht im Modell habe.
Zum Beispiel, dass Postgres sich anders verhält als meine idealisierte Tuplen-Abstraktion.
Aber abstrahieren müssen wir ja immer.
Abstrahieren ist ja irgendwie das tägliche Brot in der Informatik.
Insofern muss man dann einfach da Entscheidungen treffen.
Also wenn ich jetzt wirklich anfangen würde, dann auch noch die CPU-Semantik von x86 mit reinzunehmen.
Also es gibt Leute, die machen sowas.
Es gibt Leute, die haben die x86-Semantik formalisiert.
Aber ob ich das jetzt in unserem Projekt hätte machen wollen?
Ich glaube es nicht.
Ich glaube, das hätte nicht viel gebracht, weil dann muss ich mich auf meine Business-Domäne konzentrieren.
Ich hätte jetzt gedacht, dass du, weil du gerade mit dem Postgres-Thema anfängst, dass du dann irgendwie darauf abhebst, dass man ja im Postgres halt einen Zustand hat, also eben in der Datenbank und dass man dann so einen funktionalen Kern haben kann, der eben keine Zustände hat, sondern der eben bei einer bestimmten Eingabe eine bestimmte Ausgabe erzeugt, wie das bei funktionaler Prämien gerade so der Fall ist.
Und dass das halt ein Trick wäre, also dann gibt es ja sozusagen gar keinen State-Space.
Dann gibt es halt nur Ein- und Ausgabe-Werte.
Das hattest du jetzt aber nicht gesagt.
Genau, also State-Space heißt nicht unbedingt, dass der State veränderlich ist.
Also State-Space heißt einfach bloß, dass ich einfach mal den gesamten Space von allen Eingaben einschaue.
Und allein der ist schon hoch.
Wenn ich jetzt dann noch Mutable-State dazu nehme, dann wird es natürlich komplizierter, so wie du es richtig erwähnt hast.
Also das ist natürlich auch ein Trick, den wir oftmals machen müssen, dass wir sagen, okay, wir haben jetzt irgendwie, wir versuchen das möglichst funktional zu modellieren.
Das heißt, wir haben Input nach Output und beweisen dann eben auf dieser Pure Function ohne Mutable-State irgendwelche Dinge.
Und wenn wir dann noch irgendwie besonders interessiert sind daran, wie sich das System verändert im Laufe der Zeit, also wenn wir zum Beispiel eben eine Bestellung haben, die durch das System wandert, dann könnten wir das so machen, dass wir das als Funktion modellieren von Input nach Output und Event.
Also dass wir dann noch irgendwie so ein Event mit erzeugen als Output.
Und da gibt es ja auch schon klassische Beispiele dafür, wenn wir zum Beispiel das Event-Sourcing anschauen als Architekturmuster.
Beim Event-Sourcing habe ich ja auch so Events, die ich einfach der Reihe nach irgendwo wegschreibe.
Das ist so Immutable und ich kann dann immer den State wieder daraus rekonstruieren.
Und das ist zum Beispiel ein richtig gutes Pattern, wenn man sowas hat, um das formal zu verifizieren.
Weil dann kann ich mir einfach eine Funktion anschauen, die diesen Übergang isoliert überprüft oder durchführt.
Dann muss ich also nicht irgendwie ständig den ganzen Kontext von den 5000 alten Änderungen im Kopf behalten und das mitbeweisen.
Sondern ich habe wirklich so schön mir rausschnittene Zustandsübergänge, die ich dann fein säuberlich trennen kann.
Genau, bei Event-Sourcing ist es eben so, dass ich aus Events dann den Zustand rekonstruieren kann.
Das heißt, ich würde irgendwie abspeichern, was ich zum Beispiel alles mit einer Bestellung gemacht habe.
Und dann kann ich eben, indem ich die Sachen wieder abfahre, die Bestellung in den selben Zustand bekommen.
Und das, wie du ja sagst, führt dann dazu, dass ich da vielleicht auf dieser formalen Ebene leichteres Spiel habe.
Ich würde vielleicht noch als anderes Beispiel, um das zu illustrieren.
Also eines der Probleme, die ich habe, wenn ich imperative Programme verifizieren will, in Theorien beweisen, ist, dass ich eben diesen Heap habe, also den Hauptspeicher von meinem Programm.
Und dass ich dann ganz viele Tricks fahren muss, um irgendwie diese Speichersegmente klar voneinander zu trennen.
Weil ich könnte ja jederzeit eine Interaktion zwischen da und da haben.
Also ich könnte ja jederzeit einen Pointer haben von hier nach da.
Und dann muss ich halt irgendwie sagen, wenn ich jetzt irgendwie zeigen will, na ja, zu jedem Zeitpunkt gelten diese und diese Invarianten, dann müsste ich das immer global über den ganzen Speicher machen.
Und das ist natürlich extrem anstrengend, weil dann muss ich alle Prädikate, alle Eigenschaften immer global formulieren.
Und deswegen gibt es dann so bestimmte Tricks, zum Beispiel Separation Logic.
Separation Logic heißt Separation Logic, weil man da separatet, also man versucht dann Speicherbereiche zu trennen und dann so lokal Dinge zu beweisen und die dann hinterher zusammenzufügen.
Also, dass ich dann wirklich modular das machen kann.
Und leider sind so C-Programme im Regelfall extrem unmodular, weil ich halt immer diese Möglichkeit habe, so Pointer hin und her zu schieben.
Und da tut man sich dann natürlich wirklich schwer, wenn man sowas machen will.
Deswegen State Space reduzieren, State Space vereinfachen, Immutable ist schon mal sehr zuträglich für Verifikation.
Genau.
HappyTree581 sagt halt zu demselben Thema, also das ist eine Frage kurz nach der, die ich vorhin gestellt hatte.
Ich würde aber denken, das mit KI beweisbar zu bekommen, was man haben wollte, schon gut wäre.
Also ich denke, da geht es halt insbesondere um die Immobilisierung und um State Space, in dem Bedingungen wie keine Raketen abschießen.
Das ist so ein Meme in der funktionalen Programmierung, dass man irgendwie eine Funktion hat, die sehr sauber aussieht und sehr Immutable, aber dann als Side-Effekt irgendwo drin versteckt hat, dass man die Raketen abschießt.
Das ist so ein Running-Gag.
Also die in der Wirklichkeit keine Funktion ist, sondern eben einen Side-Effekt hat.
Genau, die noch irgendwelche Dinge macht.
Also KI ist ein interessantes Thema.
Wir haben in Isabelle schon KI gemacht, bevor es KI geheißen hat.
Und zwar, weil ich einfach versuche, automatische Beweisschritte zu haben.
Das heißt, ich schreibe hin, das ist das Theorem, das ich beweisen will.
Hier sind diese Unterschritte, also zum Beispiel per Induktion.
Und dann sage ich dem System, lauf mal los, guck mal, ob du es irgendwie ohne mein Zutun beweisen kannst.
Und das Tool in Isabelle, das nennt sich Sledgehammer.
Also ich haue dann mit dem Vorschlaghammer auf das Theorem drauf und gucke, ob noch etwas übrig bleibt davon.
Das ist ein sehr schönes Bild.
Damals haben wir das noch Machine Learning genannt, weil das System versucht hat zu lernen, welche Theoreme, welche Fakten aus der Bibliothek irgendwie relevant sind dafür.
Heute würde man das eben KI nennen.
Und ich habe vor kurzem erst wieder ein Paper gesehen, wo jemand mit KI-Unterstützung ein ganzes Mathebuch formalisiert hat.
Also die haben halt irgendwie so ein Lehrbuch genommen und haben halt irgendwie die Definitionen dann rausgeklaut und haben halt geguckt, okay, Definitionen, Satz, Beweis, Definitionen, Satz, Beweis, bla, bla, bla.
Kann ich das irgendwie mit einem LLM vielleicht automatisieren?
Und die haben da eine sehr hohe Erfolgsquote gehabt.
Also die konnten da sehr viel tatsächlich damit machen.
Und das Coole ist jetzt, wenn man sowas wie Isabelle benutzt, muss man dem LLM-Output nicht mal vertrauen.
Also man schreibt halt als Mensch die Definition hin, guckt die sich an und sagt, okay, das ist das, was ich bewiesen haben will.
Und dann kannst du machen, was du willst.
Also die LLM kann dann generieren, was sie will.
Das kann der größte Scheiß sein, in Anführungszeichen.
Solange der Isabelle Körner diesen Beweis akzeptiert, kann ich mir auch sicher sein, dass der richtig ist.
Es kann sein, dass dieser Beweis furchtbar kompliziert ist, furchtbar langwierig, furchtbar ineffizient.
Aber das ist ja egal.
Solange am Ende das Theorem rauskommt, was ich haben will, nämlich dass die Funktion sortiert, bin ich ja glücklich.
Was also bedeutet, dass die LLMs mit ihren Halluzinationen dort irgendwie durch so ein, man könnte es Harness nennen, eingefangen werden.
Und dadurch kriege ich das hin, dass dann tatsächlich nur die korrekten Beweise akzeptiert werden, weil die dann durch das Isabelle-System durchlaufen.
Genau, es könnte halt im schlimmsten Fall passieren, dass ich halt einfach keinen Beweis bekomme.
Dann weiß ich halt hinterher nicht, woran es gelegen hat, ob ich zu blöd war, ob das LLM zu blöd war oder ob es einfach nicht gilt.
Kann ja manchmal sein, dass man versucht, etwas zu beweisen, was gar nicht gilt, was einfach falsch ist.
Aber es kann nicht passieren, dass man einen halluzinierten Beweis bekommt, der dann irgendetwas Falsches beweist.
Das kann dann halt einfach nicht passieren.
Nun hatten wir ja, also ich finde es gerade spannend, nun hatten wir ja irgendwie gesagt, dass letztendlich das Beweisen von Software im Wesentlichen eine Kostenfrage ist.
Also hörte sich für mich jetzt jedenfalls an und hat gesagt, das hat eine Zeile Code, 10 Zeilen Isabelle benötigt.
Bedeutet das, dass ich durch LLMs jetzt alle meine Software tatsächlich beweisen kann?
Also weil dann muss ich die 10 Zeilen ja nicht mehr selber schreiben?
Also so weit würde ich jetzt vielleicht noch nicht gehen.
Vielleicht können wir da noch ein paar Jahre drüber reden.
Aber es ist denke ich mal so, dass die Kosten immer weiter gedrückt werden.
Also wir haben eben durch dieses damals Anführungszeichen Machine Learning schon mal einiges an Zeit eingespart.
In meinem Projekt für meine Dissertation habe ich einen Beweis drin, den ich bis heute nicht selber verstehe.
Das hat halt dieses Tool generiert.
Da werden irgendwelche lustigen Beweistaktiken rausgeholt, von denen ich noch nie was gehört habe.
Aber das ist okay.
Also ist nicht schlimm.
Aber das hat mir geholfen, diesen Beweis tatsächlich abzuschließen, indem ich wochenlang gearbeitet habe.
Und ich glaube, diese Tools werden besser.
Und die wurden auch schon vor LLMs immer besser.
Also auch da haben wir schon große Fortschritte gemacht als Community.
Ob LLMs dann nochmal das exponentiell verbessern, weiß ich nicht.
Also ich glaube es ehrlich gesagt noch nicht.
Ich glaube, wir werden da inkrementelle Fortschritte kriegen.
Und es ist halt einfach ein sehr komplexes Problem.
Es gibt ja viele Theoremen, von denen noch nicht mal ansatzweise bekannt ist, wie die Beweisstrategie auszusehen hat.
Also es gibt manchmal so große mathematisch ungelöste Probleme, wo Horden von Leuten daran gearbeitet haben.
Und das Einzige, was sie bisher geschafft haben, ist, dass sie irgendwie andere coole Sachen beweisen mussten, die wichtig und interessant sind.
Aber an dem eigentlichen Beweis wissen sie noch nicht so richtig, ob es funktioniert.
Und das ist halt so eine Sache, die man vielleicht irgendwie ein bisschen beschleunigen kann.
Aber halt nicht so, dass ich jetzt morgen meine ganze Software reinkippen kann und dann bin ich mir sicher, dass sie korrekt ist.
Was würde ich jetzt als Architekt mitnehmen?
Also was wäre tatsächlich dein Tipp an mich zu diesem formalen Methodenthema?
Was wäre mein Tipp?
Also ich glaube erstmal keine Panik.
Also es ist jetzt nicht so, dass ich jetzt ab morgen irgendwie zehn Leute einstellen muss, die jetzt Isabelle-Code schreiben können.
Das wird wahrscheinlich auch schwierig, bis morgen da zehn Leute zu finden.
Aber ein vernünftiges, sauberes Systemdesign, was so ein paar Grundlagen beachtet, sind schon mal sehr hilfreich.
Also zum Beispiel versuchen möglichst immutable zu sein, möglichst den Zustand abzukapseln, möglichst nicht zu viele parallele Threads zu haben, die sich gegenseitig in irgendwelchen State reinschreiben.
Das ist sowieso mal schwierig zu handhaben.
Und das sind einfach Dinge, die ich in der normalen Softwarearchitektur ja auch beachten sollte.
Also gerade wenn ich mal rüberschaue in das DDD-Modul, da gibt es ja auch so ein paar Sachen, dass man seine Domain-Objekte klar identifiziert.
Dann hat man seine Value-Objects, die immutable sind und dann die Interaktionen davon aufschreibt.
Und wenn man das einmal gemacht hat, ist man schon mal in einem guten Basiszustand.
Und was kann man dann als nächstes machen?
Als nächstes kann man sich mal hinsetzen.
Da kann man sich mal ans Whiteboard stellen und kann einfach mal ein paar Diagramme aufmalen.
Und kann eben mal ein Zustandsdiagramm aufmalen und kann eben mal ein Flowchart aufmalen.
Und dann kann man sich eben entscheiden, naja, vielleicht versuche ich mal, das mit einem Modelchecker durchlaufen zu lassen.
Also Modelchecker habe ich jetzt noch gar nicht erwähnt.
Da gibt es ein Tool, das heißt zum Beispiel TLA+.
Kommt von Leslie Lamport, der vielleicht dem einen oder der anderen in Begriff ist.
Weil er LaTeX gebaut hat.
Genau, und noch viele andere Sachen gemacht hat.
Und das ist zu schwer zu lernen.
Und da kann man zum Beispiel mal ein kleines Modell von der Software, also zum Beispiel so ein Zustandssystem mal reinschreiben und dann einfach mal auf Go klicken.
Das geht in VS Code.
Da gibt es ein VS Code Plugin dafür.
Kann man ein bisschen rumspielen damit und kann dann zum Beispiel schon mal ein paar Sachen lernen.
Zum Beispiel sagt dann das Tool, hey Moment mal, hast du schon mal darüber nachgedacht, was passiert, wenn du im Zustand X bist und dann Y passiert?
Und das ist dann zwar noch kein richtiger Beweis, weil TLA++ ist kein Beweiser.
Das ist bloß ein Modelchecker.
Also ich sage jetzt bloß, das war jetzt nicht abwertend gemeint.
Das ist ein cooles Tool.
Oder ich gehe dann halt einfach dann zurück an das Whiteboard und sage, ich muss jetzt noch mal hier was anpassen.
Damit habe ich schon mal viel gekonnt.
Also das ist schon mal ein Akt, mit dem ich mir über meine Software Gedanken mache und dann vielleicht Fehler finde, bevor ich sie überhaupt implementiert habe.
Okay, was bedeutet, dass ich dadurch sozusagen in Modellierungsprozessen unterstützt werde, ist eigentlich deine Aussage.
Richtig, genau.
Das ist auf jeden Fall etwas, was vor der Implementierung passiert.
Es gibt ja diese Daumenregel, nicht Kryptografie will ich nicht selber implementieren, weil wenn ich Kryptografie selber implementiere, dann habe ich zwar vielleicht den abstrakt korrekten Algorithmus, der irgendwie auch schwer zu brechen ist.
Aber weil wir halt als Entwickler so wahnsinnig schlecht sind, kann man davon ausgehen, dass wir wahrscheinlich einen Fehler einbauen, der dann dazu führt, dass das vielleicht irgendwie doch gehackt werden kann.
Ist es sinnvoll, daraus abzuleiten, dass wenn ich sozusagen ein System formal beweisen will, dass ich es dann lieber nicht selber schreiben sollte?
Also weil das sozusagen die Komplexitätsklasse übersteigt, die ich als normaler Entwickler selber lösen sollte.
Und ich sollte eher versuchen, eine Library zu benutzen, die das halt irgendwie tut.
Also zu einem gewissen Grad würde ich zustimmen.
Ich meine, es implementiert ja auch keiner seine eigene Datenbank.
Also vielleicht macht das ja jemand, aber es gibt zum Beispiel Leute, die schauen sich Datenbanken, insbesondere verteilte Datenbanken, kritisch an mit solchen Tools und gucken, ob sie dann irgendwelche Sachen fixen können.
Aber für die Business-Logik gilt das natürlich nicht.
Also ich werde von meiner Business-Logik jetzt nicht irgendwie was von der Stange nehmen können.
Ich meine, ich kann natürlich dann irgendwelche Konsultants einkaufen, die mir das dann machen.
Aber ich glaube ehrlich gesagt, dass man viele Sachen auch lernen kann.
Also vielleicht kann man jetzt nicht Isabelle von einem Tag auf den nächsten lernen.
Aber es gibt schon auch formale Methoden, die man relativ unaufwendig, also ich sage relativ, nicht komplett unaufwendig, sondern relativ unaufwendig einsetzen kann.
Und wie gesagt, da würde ich einfach dazu raten, keine Angst zu haben.
Und das Schöne ist ja, wenn das Tool dann sagt, das ist korrekt, dann kann ich mir halt auch relativ sicher sein, dass es auch wirklich stimmt.
Also es ist jetzt dann nicht so, dass ich hinterher dann gar nicht mehr schlauer bin.
Was ich natürlich nicht machen sollte, ich sollte dann natürlich nicht zu meinem Kunden gehen und sagen, pass mal auf, ich habe das alles korrekt bewiesen und du wirst niemals einen Fehler drin finden.
Das ist alles super.
Das sollte man nicht machen.
Also man muss dann halt auch gucken, wo sind dann die Einschränkungen, wo können dann trotzdem noch Fehler lauern.
Zum Beispiel, wenn ich jetzt irgendwie nur ein Modell korrekt bewiesen habe oder ein Modell verifiziert habe, dann kann es halt sein, dass ich in meiner Implementierung in Java halt irgendwie einen Bug drin habe oder ich habe halt irgendwie einen JDK-Bug mit drin.
Das kann halt immer noch passieren.
Selten, aber solche Sachen können dann halt passieren.
Dafür brauche ich jetzt wahrscheinlich Menschen mit einer ganz besonderen Ausbildung.
Also du hast ganz viel über Isabelle gesprochen und hast ja offensichtlich in dem Bereich promoviert.
Woher kriege ich denn solche Leute für mein Team?
Weiß nicht.
Man könnte vielleicht ab und zu ein paar Leute mit Mathestudium mal mit reinnehmen ins Team.
Also es ist nicht so einfach, Leute zu finden, die das alles im Hintergrund haben, die damit schon Erfahrungen gesammelt haben.
Das muss man einfach ganz klar sagen.
Aber ich denke, man kann auch Leute ausbilden in die Richtung.
Also wenn ich jetzt wirklich einen Bedarf habe und da vielleicht mal einen Test machen will damit, also einfach mal vielleicht irgendwie einen bestimmten Bereich meiner Software nehmen möchte.
Es gibt Lehrbücher, also genauso wie es halt Java-Lehrbücher oder Springboot-Lehrbücher gibt, gibt es halt auch zum Beispiel für TLA-Plus-Lehrbücher.
Ein Bekannter von mir arbeitet gerade an einem Buch, der nennt sich Logic for Programmers.
Da stehen eben auch solche Dinge drin, wie man zum Beispiel Prädikaten-Logik-Sachen formalisieren kann.
Und das kann man sich halt mal anschauen.
Und dann ist man vielleicht nicht so superproduktiv, genau wie man eine neue Programmiersprache lernt, dann nicht so superproduktiv ist gleich am Anfang.
Aber das sind Sachen, die kann man sich schon anschauen.
Also ich würde dazu raten, einfach mal mit einer gesunden Naivität ranzugehen und mal zu gucken, wie weit man kommt.
Ich glaube, der Bekannte von dir ist der Hillel Wayne.
Genau, den hatten wir auch schon.
Der ist auch ein ganz großer Fan von TLA-Plus und Model-Checking und solchen Sachen.
Und der hat da einige gute Ressourcen dafür im Angebot.
Aber er ist nicht der Einzige.
Also ich will jetzt nicht irgendwie da das Buch promoten.
Also es ist ein gutes Buch, aber es gibt da auch noch einige andere Ressourcen für sowas.
Du bist ja jetzt einer der Korrekturen für den formalen Methoden-Lehrplan beim ISAKoB.
Michael Sperber hatten wir schon genannt als eine andere Person.
Die hatten wir ja auch schon im Stream zum Thema, wo wir tatsächlich ein System durchgebaut haben mit funktionaler Programmierung.
Und wir hatten, glaube ich, eine grundlange Episode mal mit ihm mit funktionaler Programmierung.
Ich erinnere mich, dass wir da zusammengesessen haben.
Und dann ist es noch die Isabellela Stelkerich, wenn ich es richtig sehe.
Was machst du, was macht ihr in dieser Rolle?
Als Kuratoren von dem Lehrplan.
Ich habe mal ganz schnell gesagt, wir haben den Lehrplan entwickelt.
Das heißt, wir haben uns an der Entwicklung des Lehrplans auch noch ein paar andere Leute beteiligt.
Da will ich jetzt mal hier nicht unter den Teppich kehren.
Also es war auf jeden Fall ein Team-Effort.
Wir haben uns zusammengesetzt.
Wir haben, glaube ich, angefangen mit so ein paar Miro-Boards, wo wir ein paar Stickys gemacht haben.
Was glauben wir denn, was Leute über formale Methoden wissen sollten.
Wir haben ein paar Themen zusammengetragen und dann Schritt für Schritt das dann als Lehrplan formuliert.
Und das Schlimmste daran ist, eigentlich die Sachen zu streichen, weil man kann natürlich beliebig lang über diese Themen philosophieren.
Und dann haben wir gesagt, okay, wir machen jetzt nicht konkrete Tools.
Wir können vielleicht, also in einem Lehrplan können natürlich immer Beispiele genannt werden oder in einer tatsächlichen Toolung können Beispiele genannt werden.
Aber wir schreiben zum Beispiel jetzt nicht vor, man muss einen Isabelle-Workshop machen oder sowas.
Das heißt, wir haben im Prinzip aus diesem Miro-Board dann Schritt für Schritt wieder Sachen rausgestrichen und gesagt, was ist eigentlich das Minimum, was ein Software-Architekt wissen muss, um Systeme so zu designen, dass sie verifizierbar sind und dass ich formale Methoden darauf anwenden kann.
Und dann eben auch noch als zweiten Schritt auch bestimmte formale Methoden zumindest erstmal kenne, dass ich also dann genau weiß, wo ich weiter forschen muss, um dann mein System bestimmte Korrektheits-Eigenschaften beweisen zu können.
Also einmal die Art und Weise, wie Sie Architektur bauen, um solche Methoden einsetzen zu können, dann hat ein Überblick über diese verschiedenen Methoden.
Genau.
Aber es ist eben ganz wichtig, dass wir hier keinen Tutorial für irgendeine formale Methode machen, weil das natürlich auch nicht die Aufgabe originär von dem Isacube-Modul ist.
Also wir machen ja da keine Java-Schulungen und keine Isabelle-Schulungen, keine sowas Schulungen.
Also es geht ja immer darum, dass man den mal aus einer hohen Flughöhe im Überblick hat, was da alles so an Möglichkeiten besteht.
Genau, Powerpoint-Architekturwissen.
Ich glaube, da sollten wir auch noch kurz erwähnen, so ein Lehrplan ist eben ein Lehrplan.
Das heißt also, die jeweiligen Anbieter dieses Moduls können den dann unterschiedlich ausführen und können sich irgendwie unterschiedlich überlegen, wie sie es halt umsetzen können.
Auch mit unterschiedlichen Werkzeugen, aber auch die Sachen auch in unterschiedlicher Reihenfolge vermitteln usw.
Und auch Übungen.
Ich gehe da stark davon aus, wenn man diese Schulung besucht, dass man da bei den meisten Schulungsanbietern irgendwie Prädikatenlogik zumindest mal hinschreiben sollte und man ein paar Sachen definieren sollte.
Also das ist nicht reines Zuhören.
Da muss man dann auch mal ein paar Formeln durchboxen.
Wie hängt das mit anderen Lehrplänen aus dem ESA-Cubier-Universum zusammen?
Ja, also es gibt schon so ein paar Überschneidungen oder ein paar Referenzen zu anderen Lehrplänen.
Also DDD hatte ich zum Beispiel schon erwähnt.
DDD ist deswegen relevant, weil ich dort lerne, wie ich eine saubere Domain-Modellierung mache.
In eine ähnliche Richtung geht das mit dem Domain-Specific-Languages-Lehrplan.
Das heißt, ich schaue mir irgendwie meine Business-Domäne an und versuche dann erstmal ein Vokabular zu finden, dass ich darüber reden kann.
Also ich muss irgendwie mir ganz klar machen, was heißt es denn, eine Bestellung zu haben?
Was heißt es denn, dass die von einem Zustand in den nächsten geht?
DDD geht natürlich eher so in Richtung Discovery.
Also wie kann ich das explorieren?
Wie kann ich das rausfinden?
Wie kann ich das hinschreiben?
DSL geht dann darum, wie kann ich es dann zum Beispiel in einer schönen algebraischen Art und Weise hinschreiben?
Und dann gibt es auch noch die funktionale Architektur, wo ich mich um so etwas wie Immutability, Zustandsmodellierung und sowas kümmere.
Ich sehe da schon irgendwie einen roten Faden.
Also wir werden da immer formaler, mehr oder weniger, in dieser Richtung.
Und wie ich schon erwähnt hatte, wenn man sich an diese Richtlinien hält, wenn man eben sauber seinen Zustandsraum modelliert, wenn man versucht, immutable zu sein und so weiter, dann hat man schon mal eine gute Grundlage geschaffen.
Und eine Referenz würde ich noch kurz erwähnen in dem Embedded-Bereich.
Da gibt es ja auch zwei Lehrpläne, glaube ich, mittlerweile, Embedded und Embedded Security.
Da ist formale Verifikation auch sehr häufig anzutreffen.
Das heißt, wenn man da als Architekt oder als Architektin in diesem Bereich unterwegs ist, dann glaube ich, kann man das auch sehr gut kombinieren, das Wissen.
Gerade im Embedded-Bereich hat diese Geschichten, wo ich halt versuche, Dinge zu steuern und das ist irgendwie nicht cool.
Genau, das ist wie gesagt das Flugzeug.
Das möglichst nicht durch Null dividieren.
Der Nils Brodersen hat bei LinkedIn eine Frage gestellt.
Die ist, glaube ich, nicht so ganz im Kern der Diskussion, aber mal schauen.
Also die Frage oder die Aussage ist, ich wage mal die These, dass Softwareentwicklung in Zukunft 80 oder mehr Prozent aus strategischem Denken und einem tiefen Verständnis der Zusammenhänge in Vorbereitung auf Software besteht.
Wie seht ihr das?
Rolle ein eher AI-Solution-Architekt als Entwickler?
Also ich würde zu 80 Prozent der Frage zustimmen.
Das strategische Denken und das tiefe Verstehen der Zusammenhänge bin ich ein großer Fan davon.
Nämlich erstmal zu gucken, was man eigentlich baut, bevor man es tatsächlich baut.
Ich höre oftmals als Vorurteil, naja, das ist ja irgendwie gar nicht agil, aber ich glaube, das muss das eine oder andere nicht ausschließen.
Also natürlich können sich Requirements ändern, aber es ist halt auch wichtig, dass man Requirements erstmal versteht und auch die Domäne erstmal gut versteht.
Ob man dann in Zukunft bloß noch den Kontrakt der Software hinschreibt und dann die AI eine korrekte Implementierung daraus generiert, da bin ich mir jetzt noch ein bisschen skeptisch dazu.
Also das ist der 20 Prozent, wo ich mir nicht so ganz sicher bin.
Aber wenn man halt wirklich Wert darauf legt, dass man qualitativ korrekte Software hat, dann wird kein Weg daran vorbeiführen, dass man das tief verstehen muss.
Also das ist irgendwie die Grundvoraussetzung dafür.
Also ich fühle mich da sozusagen auch angesprochen.
Und ergänzend zu dem, was du gesagt hast, ich würde sowas eigentlich auch unterschreiben.
Also einmal, ich bin nicht sicher, ob das was mit formalen Methoden zu tun hat.
Das ist halt so ein bisschen ein Fragezeichen.
Dennoch ist es ja eine interessante Frage.
Ich glaube, das Einzige, was mir hier so ein bisschen aufstößt und tatsächlich auch etwas ist, wo ich Probleme habe mit unserer Branche, das ist die implizite Annahme, dass Entwickler so nicht agieren.
Und mindestens das, was du genannt hast, Lars, mit ich muss halt die Requirements verstehen, ist eigentlich das, was Entwickler in meiner Ansicht nach auszeichnet.
Und ein Problem, was ich mit dieser AI-Debatte habe und das klingt hier ein bisschen an, ist die Reduktion von Entwicklern auf Menschen, die halt Code ausstoßen.
Das ist halt einfach nicht so.
Und da gibt es halt so zwei Sachen, die ich da erwähnen möchte.
Das eine ist irgendwie diese Episode, die ich vor einiger Zeit gemacht habe, von wegen Programmierung als Modellbildung, Quatsch, als Theoriebildung, basierend auf dem Paper von dem Peter Nauer, wo er im Prinzip sagt, das hat Entwickler in eine Theorie erzeugen darüber, wie das System mit der realen Welt interagieren soll.
Und dass das tatsächlich der zentrale Punkt ist, den man auch nicht so einfach hinschreiben kann in der Dokumentation.
Der hat auch nicht Teil des Codes.
Und das ist etwas, was eben bedeutet, dass ich als Entwickler nicht nur Code produziere, sondern mehr.
Also ein Modell darüber, wie das alles funktionieren soll, wie das in die Welt geht.
Und ich bin da halt auch, das ist so die andere Sache, wir waren ja tatsächlich mal gemeinsam bei einer Firma und unsere damalige Kollegin, die Joy Heron, hat so einen schönen Artikel geschrieben im Inokio Blog, wo halt letztendlich drin stand, also cool, dass halt AI, ich paraphrasiere und ich hoffe, sie sieht mir das nach, wo sie im Prinzip gesagt hat, cool, dass die AI mir jetzt irgendwie Buttons baut und so.
Ich muss halt, ich kann mich deswegen um die Dinge kümmern, die ja tatsächlich relevant sind und ich eben verstehen, was eigentlich die Fachlichkeit ist.
Und das, finde ich, ist halt sehr unaufgeregt, eine sozusagen Richtigstellung darüber, was halt Entwickler tatsächlich tun.
Genau, ich würde vielleicht noch einen Satz dazu sagen, nämlich was du gemeint hast, diese Theoriebildung, die nicht im Code steht und vielleicht auch nicht in der Doku, mit formalen Methoden versuchen wir das explizit zu machen.
Also wir versuchen dann eben auch diesen ganzen Hintergrund, was da alles so mitschwingt, in mehr oder weniger ein formales System zu gießen, was vielleicht aussieht wie Code oder vielleicht eben auch nur auf dem Papier ist.
Und dann uns eben, dann eben auch das kommunizieren können, was wir uns eigentlich dabei gedacht haben und warum macht das System das, was es macht.
Ja, weil wir eben fünf Invarianten haben, die irgendwie berücksichtigt werden müssen.
Ja, und an der Stelle fand ich mich halt auch erinnert an diese Sache, die mich schon länger so ein bisschen umtreibt.
Also vielleicht ist es gar nicht das Artefakt, was so relevant ist, sondern dass ich das Artefakt erzeuge.
Also vielleicht ist nicht die State Machine das Entscheidende und dass die halt irgendwie fachlich, also dass ich die jetzt irgendwie formal beweisen kann und zeigen kann, die hat halt x, y und z als Eigenschaften, sondern dass ich mich überhaupt erstmal hinstelle und das Ding baue oder vielleicht sogar mit Leuten drüber rede.
Das ist ja auch das, was du gesagt hast.
Und dann halt nennen wir, gibt es Produziere und das ist eben ja eine soziale Geschichte.
Also das ist gerade nicht so, dass ich jetzt sage, das ist halt das Artefakt, wir sind jetzt alle fertig, sondern da ist es eben so, dass ich halt diesen Prozess habe, wo ich es halt hinschreibe.
Das hilft mir halt und ich kann es mit anderen Leuten kommunizieren.
Und das ist etwas, was mir, wo ich zunehmend der Meinung bin, dass das vielleicht wichtiger ist.
Also wir können sozusagen die State Machine wegwerfen und dadurch, dass wir drüber geredet haben, haben wir trotzdem einen Vorteil.
Das ist halt so der Punkt.
Absolut.
Würde ich sofort unterschreiben.
Genau.
Und ich weiß nicht, ob du noch Dinge hast, die du sozusagen zum Abschluss loswerden wolltest?
Eigentlich ist das ein ganz gutes Schlusswort.
Da sind wir wieder rausgekommen, dass Programmieren sehr oft eine soziale Tätigkeit ist.
Selbst wenn man halt versucht, über formale Methoden zu sprechen.
Absolut, ja.
Gut, dann würde ich sagen, vielen Dank.
Nochmal der Hinweis auf das ISR-KUBI-Sozialpädagogikulturforum vom 16. und 17.
Juni.
Und da haben wir beide Vorträge.
Wir werden auch, denke ich, noch Episoden in der Vorbereitung haben.
Und dann eben insbesondere das Panda darüber, wie LMS denn nun das Lernen beeinflusst.
Dann bis dahin.
Und ich hätte jetzt fast gesagt, schönes Wochenende ist ein bisschen früh.
Also es ist noch nicht Freitag, aber weiterhin einen guten Start in die Woche wäre, glaube ich, der richtige Ausgang.
Also schönen Abend.
Das würde durch den Typchecker durchgehen, aber schönes Wochenende heute nicht.
Es ist immer vor dem nächsten Wochenende.
Ja, das stimmt.
Ja, bis dahin.
Danke.
Tschüss.
Tschüss.
Hier ein Hinweis in eigener Sache.
Softwarearchitektur im Stream ist live vor Ort.
Wir sind beim ISR-KUBI Softwarearchitekturforum im Juni in München dabei.
Mehr Infos dazu und einen speziellen Rabattcode für unsere Community findest du auf unserer Website software-architektur.tv.
Sei dabei, stell Fragen und komm auch gern auf uns zu.