# Strategic ROI of Formal Software Verification

**Podcast:** Software Architektur im Stream
**Published:** 2026-04-28

## Transcript

Herzlich willkommen zu einer weiteren Episode von Software-Architektur im Stream.
Lars, und da haben Sie ja gerade eben schon die Vorankündigung, also Lars, wie auch ich, werden auf dem ESLQB Software Architecture Forum sein.
Lars hat einen Vortrag, ich hatte einen Vortrag und außerdem haben wir auch noch ein Panel, was wir gemeinsam mit einem Partner machen zum Thema Lernen und LMs.
Und ein bisschen das Thema von heute, so ein bisschen auch, glaube ich, hat was 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 Huppel.
Ich arbeite bei Giesecke und Devrient 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 hattest 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 CSVR hat vielleicht was mit Funktionale Programmierung zu tun.
Könnte sein, ja.
Genau.
Dann können wir loslegen mit der Frage, was sind denn überhaupt formale Methoden?
Und ich glaube, du hattest da so eine schöne Grafik mitgebracht.
Genau, also formale Methoden, es ist so, also 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 so 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 und die Y-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 Theorembeweise.
Hat vielleicht der eine oder die andere schon mal was davon gehört?
Also ein Theorembeweise, 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 hier mal 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 erstmal irgendwie abstrakt hinschreiben, 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, First oder Logic, 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 schon mal benutzt haben, ist links oben nämlich ein Typsystem.
Also ein Typsystem ist auch eine bestimmte harte noch formalen Methode, weil da muss ich gegenüber dem Computer rechtfertigen, dass das, was ich gemacht habe, auch einigermaßen wichtig ist.
Also ein Typsystem stellt nicht sicher, dass meine Implementation wirklich korrekt ist, aber stellt zumindest mal sicher, dass ich jetzt nicht hier irgendwie, keine Ahnung, Okay, 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.
Zum Beispiel 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.
Bei dem, 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 halt einen String erwartet und ich gebe dem halt ein 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 Laufzeit oder dynamisch zur Laufzeit in mir hinbekomme.
Und das ist jetzt das Erste, was mir eingefallen war, weil du sprachst über sowas wie das Kanalpointer da ist.
Genau.
Richtig.
Also genau, da hast du mal einen wichtigen Begriff genannt.
Also das meiste handelt...
sich wirklich um statische Analysen.
Das heißt, alle diese Sachen, die ich hier auf der Folie habe, die sind tendenziell überwiegend ohne Runtime.
Das heißt, das sind alles Sachen, die mache ich, indem ich mir den Code anschaue.
Und das führt eben dazu, dass ich ahead of time, also ohne dass ich die Inputs, 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 irgendwie 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 abzudecken und uns abstrakt Gedanken zu machen, was kann denn alles passieren und das dann irgendwie berücksichtigen.
Was denn bedeutet, dass diesbezüglich statische typisierte Sprachen sozusagen die bessere Wahl sind, weil sonst würde ich erst zur Laufzeit rausbekommen, 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 irgendwie 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 Implementationenaussagen treffen will, dann...
Ja, reicht das vielleicht nicht.
Genau, dann warst du auf First Logic eingegangen und hattest dann aber als Beispiel sofort eine State Machine genannt.
Also 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 erstmal 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 bestimmte, also mehr oder weniger beliebige Sachen ausdenken in diesen Fällen, wie man das jetzt genau modelliert.
Und hattest du ja gesagt, dass ich beispielsweise für diese, also nicht eine State Machine, wir hinten waren 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 irgendwie 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.
Wenn man jetzt jemanden fragt, der Theorembeweiser benutzt, also der wie ganz rechts oben in der Ecke ist, also wie ich zum Beispiel in meiner Forschungsarbeit gemacht habe, dann würde ich natürlich sagen, ja, Moment mal, also damit kann ich jetzt irgendwie noch nicht so wahnsinnig viel beweisen über meine Software.
Also das ist jetzt dann irgendwie gar nicht implementierungsnah, das ist jetzt nur irgendwie ein Modell.
Und das stimmt natürlich auch zu einem gewissen Grad.
Und trotzdem ist es so, dass wenn ich überhaupt erstmal nachdenke, welche Zustände meine Software überhaupt mal einlegen kann, also allein die Tatsache, dass ich jetzt irgendwie drü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 der Bestellung?
Also was sind da 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 Syntax und Semantik hat und ich dann bestimmte Aussagen dann auch wirklich treffen kann.
Also bei Zuständungsmaschinen 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 Type-Checker 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 ist auch ein bisschen Sinn, diese 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.
Genau, jetzt hattest du schon mehrfach sozusagen als sehr mächtiges Werkzeug diese Theorie Improver 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, ja, 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 einem Theorembeweiser diese Sortierungsfunktion implementieren.
Jetzt gibt es von diesen Theorembeweisern auch viele verschiedene.
Ich nehme mal als Beispiel Isabel, weil mit Isabel kenne ich mich am besten aus.
Das ist halt einfach das System, was wir benutzt haben in der Uni.
Isabel ist im Prinzip eine funktionale Programmiersprache.
Das heißt, ich würde...
Stell dir mal vor, man nimmt irgendwie eine Sortierfunktion, die man in Skala geschrieben hat oder in Haskell, dann kann man die relativ 1 zu 1 nach Isabel übersetzen.
Also man tippt dann halt auch einfach Funktionsdefinitionen, Datentypdefinitionen, kann dann rekursiv irgendwelche Dinge tun.
Dann hat man erstmal nur die Funktion, die kann man auch ausführen, aber dann hat man noch nichts bewiesen.
Und dann kann man eben in Isabel 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 Isabel, ja cool, du musst das jetzt beweisen.
Und dann sage ich Isabel, 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 sage ich Isabel, ah cool, du machst das per Fallunterscheidung.
Dann gib mir doch mal den Fall, was passiert, wenn die leere Liste reinkommt.
Dann gib mir doch mal den Fall, was passiert, wenn die nicht leere Liste reinkommt.
Also im Prinzip kriege ich dann so das Aufgefaltete rein und ich kann dann so immer rein zoomen.
Und das muss ich dann als User machen.
Also wenn ich dann Isabel 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.
Also 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 könnte 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 dieser Rekursionsaufruf muss ich noch eine Annotation dran machen, wie sich das Argument verhält, wie auch immer.
Das ist nicht das, was ich in Isabel mache.
In Isabel 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 irgendwie 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 Isabel 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 zwei Tieralgorithmen genannt, was ich da vielleicht irgendwie benutzen will, weil ich halt irgendwie absichern will, dass halt eine 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 Softwarearchitektur, mit Softwareentwicklung 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.
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, also man muss natürlich einschränken, also eine State Machine habe ich schon mal aufgemalt, darüber nachgedacht, dass das halt irgendwie sozusagen schief sein kann.
Das ist halt, das ist, glaube ich, relativ klar.
Vielleicht ist das auch schon ein Ergebnis von der Episode.
Aber sowas wie ein Theorem-Prover 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 Diagrammen komme, desto teurer wird es.
Es gibt ja schon Leute, die finden Typsysteme nicht gut, weil sie dann irgendwie, also in Rust ist das ja immer so ein Meme, dass man irgendwie länger braucht, um dann den Typ-Checker zufrieden zu stellen, als den eigentlichen Code zu schreiben.
Und je weiter dann nach oben rechts kommt eben, also sowas wie Isabel zu benutzen, ist halt sehr aufwendig.
Warum?
Weil ich sehr viel mehr Aufwand in die Implementierung stecken muss.
Also es gibt da immer so verschiedene Faustformeln, die da so rumgeistern.
Eine Faustformel ist, dass so auf eine Zeile Code so zehn Zeilen Verifikation kommen.
Also zehn Zeilen so Isabel-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 sind oftmals Software, wo ich mir eben nicht erlauben kann, dass irgendwie ein Fehler drin ist.
Und weil ich gerade von der App geredet habe, 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 dann halt auch manchmal ganz klar wirtschaftlich denken und sagen, okay, für diesen Teil von meiner Software, das ist vielleicht einfach gar nicht relevant.
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 an 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.
Genau, und dann hat er oder sie auch gleich noch eine Frage gestellt.
Haben die Theorie-Improver eigentlich das Problem, dass auch mit Tests aufkommen kann, woher weiß ich, dass mein Proof keinen Fehler hat?
Da kann ich eine schöne Anekdote dazu sagen.
Es gab bei uns am Lehrspiel immer so das Motto Beweis durch korrekte Definition.
Was heißt das?
Also je nachdem, wie ich meine Definition mache, also ob ich jetzt irgendwie die Sortierfunktion so definiere oder anders definiere oder meine...
meine Korrektheitseigenschaften so definieren oder anders zu definieren, kann das sein, dass der Beweis sehr einfach oder sehr schwierig wird.
Man kennt das ja, manchmal versucht man irgendwie sehr kompliziert irgendwas 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.
Und sowas kann eben bei formalen Beweisen auch passieren, dass also die Definitionen einfach sehr wichtig sind, also wirklich tragende Säulen sind.
Und dann habe ich manchmal zwei Definitionen, die sehen irgendwie fast ähnlich aus oder sind dann subtil anders.
Konkretes Beispiel.
Und die, die Mathe studiert haben, müssen jetzt mal kurz die Ohren zuhalten.
In Isabel 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.
Also 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.
Und dann denken die so, hä, warum kann ich denn das jetzt beweisen?
Das ist doch irgendwie Division durch Null.
Und es ist natürlich so gestrukturiert, dass man anderswo dann 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?
Und also 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.
Also die Architektur von diesen Theorienbeweisern ist so gebaut, dass ich eben diesen Kernel habe.
Und der Kernel ist relativ klein.
Also dass praktisch der Kernel einen Bug hat, der dafür sorgt, dass mein Beweis durchläuft, obwohl er gar nicht durchlaufen sollte, das ist extremst selten.
Das kommt alle zehn Jahre vielleicht einmal vor.
Aber das ist wirklich...
Die meisten Fehler entstehen dadurch, dass man einfach Dinge beweist, die was anderes sind, als man geglaubt hat, was man bewiesen hat.
Was sich halt so anhört wie, also ich weiß gar nicht, wo ich das aufgeschnappt habe, dass mathematische Beweise eigentlich auch nur ein soziales System sind.
Und da müssen halt Leute drüber gucken.
Und erst wenn eben genügend Leute drüber geguckt haben, dann ist es eben ein offiziell richtiger Beweis.
Insbesondere bei diesen nicht trivialen Beweisen, die halt irgendwie über Seiten und Seiten gehen.
Das kann ich durch Theorembeweise ein Stück weit noch unterstützen, indem ich halt sage, okay, wenigstens sind die logischen Schlusswirkungsschritte korrekt.
Aber wenn jetzt jemand reingeht und sagt, ich definiere mir jetzt irgendwie meine abstruse Mengen, Mannigfaltigkeits, Faserbündel, Gedöns irgendwie anders als alle anderen das definiert haben, dann habe ich halt irgendwie nichts bekommen dabei.
Genau.
Das Slam hat geschrieben, danke, also kein Proofprover.
Ah, da muss ich auch wieder Jein sagen, weil Isabel 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 Rheinraum 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 Proof-Prover und dann kann man sich die Frage stellen, gibt es einen Proof-Prover-Prover?
Also irgendwie muss es dann auch mal aufhören, 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 Kernel-Bugs möglichst ausschließen zu können.
Es gab vor allem, also wir haben ja bei Software Architektur im Stream dieses Formular auf der Webseite, wo man nämlich Fragen stellen kann.
Und da gab es vorher, ehrlich gesagt, ziemlich langer 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 halt, ein Ding zu einer Query reingebaut, mit eben den ganzen Remote-Code-Exploits, wo ich also einem System sage, nicht, führ 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 dem Diagramm, im Typsystem schon sehr viele Sachen ausschließen kann.
Beispielsweise kann ich jetzt in Rust nur sehr, sehr schwer hinkriegen, dass ich irgendwie überspeichert 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 bugfrei, aber es können halt solche Sachen in Rust schwieriger zu exploiten.
Das ist also die erste Antwort.
Und die zweite Antwort ist, es gibt...
auch die, die in C geschrieben sind, die genau diese Dinge, wobei genau diese Dinge verifiziert werden, in Isabel beispielsweise oder in anderen Tools.
Ich habe mal zwei Beispiele mitgebracht.
Also ein Beispiel wäre ein Mikro-Kernel von einem Betriebssystem.
Da rede ich jetzt wieder von einer anderen Art von Kernel.
Also ein Betriebssystem-Kernel, da gibt es ein Betriebssystem, das heißt L4.
Und das ist so eine Mikrokernel-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 also 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 Anwendungsfelder.
Damit hat man aber sozusagen im normalen Software-Engineer vielleicht nichts zu tun.
Ich glaube, wir sollten erwähnen, nicht Micro-Carnel als Micro-Carnel, weil ich glaube, der kann nur Tasks-Switching oder sowas nicht, also ganz wenig Funktionalität.
Genau, also der macht halt das typische Speicherallokation und Verwaltung, Prozesse starten und managen und Interprozesskommunikation.
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.
Und 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 CompSare-Projekt.
oder ComCert, je nachdem, ob man es Französisch oder Englisch ausspricht.
Das ist in einem anderen Theorienbeweiser gemacht, also das SEL4 wurde in Isabel 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ührt zumindest keine neuen Bugs ein.
Und dann kann man so spaßige Sachen beweisen, dass irgendwie Compiler-Optimierungen korrekt sind.
Weil im GCC ist halt oftmals so ein Ding, dass der abstruse Optimierungen implementiert und die sind dann halt vielleicht falsch oder funktionieren nur in zwei Prozent der Fälle falsch oder sowas.
Und das ist dann halt schon etwas, was in der Industrie auch benutzt wird.
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, da hast du es wahrscheinlich.
Aber es gibt auch so, der Mike Sperber benutzt, der ist ja auch Co-Kurator von dem FM-Modul, dem ISACO-B, der benutzt immer das Beispiel mit dem Tacho.
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 Theorienbeweise, aber halt andere Methoden, um sowas sicherzustellen, dass man einfach standardkonform ist.
Also es gibt bestimmte Standards, Regulatorik, und dann muss man eben beweisen auf einem bestimmten Level, dass man diese Standards erfüllt.
Und dann kann man nicht einfach nur ein Dokument abgeben und dann muss man halt wirklich ein rigoroses Argument liefern.
glücklicherweise sage ich mal fast, Sachen, mit denen wir uns nicht immer zu ständig überall behängen müssen.
Das ist halt dann schon für sehr spezielle Anwendungsfälle.
Genau, also letztendlich 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 anzuleben.
Es gibt eine Frage von HappyTree5812 und die Frage ist, ist nicht am Ende wie immer das Problem, dass das 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 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 den 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 was auch immer 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 Tupeln 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 Implementierung irgendwas habe, was ich nicht im Modell habe.
Also dass zum Beispiel das Postgres sich anders verhält als meine idealisierte Tupelabstraktion, was auch immer.
Aber abstrahieren müssen wir ja immer.
Also abstrahieren ist ja irgendwie das täglich 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 ich muss mich halt auf meine Business-Domäne konzentrieren dann.
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 ja bei funktionaler Programmierung so der Fall ist.
Und dass das halt ein Trick wäre, also dann gibt es ja sozusagen gar kein State Space, dann gibt es halt nur Ein- und Ausgabewerte.
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 versuchen das möglichst funktional zu modellieren.
Das heißt, wir haben Input nach Output.
Und beweisen dann eben auf dieser Pure Function ohne Mutual 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.
ständig den ganzen Kontext von den 5000 alten Änderungen im Kopf behalten und das mitbeweisen, sondern ich habe wirklich so schön mir rausgeschnittene Zustandsübergänge, die ich dann fein säuberlich trennen kann.
Genau, also bei Eventsourcing 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 irgendwie auf dieser formalen Ebene leichteres Spiel habe.
Ich würde vielleicht noch als kurz ein anderes Beispiel, um das zu illustrieren.
Also eines der Probleme, die ich habe, wenn ich imperative Programme verifizieren will in Theorembeweisern, ist, dass ich eben diesen Heap habe, also den Hauptspeicher von meinem Programm, und dass ich dann ganz viele Tricks fahren muss, um irgendwie diesen...
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, naja, 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.
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, dass mit KI beweisbar zu bekommen, was man haben wollte, schon gut wäre, also ich denke, da geht es halt insbesondere um die Immunitierung und um State Space, mit den 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, der in Wirklichkeit keine Funktion ist, sondern eben ein Side-Effekt hat.
Genau, operativ noch irgendwelche Dinge macht.
Genau, also KI ist ein interessantes Thema.
Wir haben in Isabel 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 Isabel, das nennt sich Slashhammer.
Also ich hau dann mit dem Vorschlaghammer auf das Theorem drauf und gucke, ob noch was übrig bleibt davon.
Das ist ein sehr schönes Bild.
Und damals haben wir das noch Machine Learning genannt, weil das System irgendwie 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 rausgeklaubt und haben halt geguckt, okay, Definition, Satz, Beweis, Definition, 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 Isabel benutzt, muss man dem LLM-Output nicht mal vertrauen.
Also man schreibt halt als Mensch die Definition hinguckt, 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 Isabel 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 LMs mit ihren Halluzinationen dort irgendwie durch so ein, man könnte es Harness nennen, eingefangen werden.
Und dadurch kriege ich das halt hin, dass dann sozusagen tatsächlich nur die korrekten Beweise akzeptiert werden, weil die halt dann durch das Isabel-System durchlaufen.
Genau, also es könnte halt im schlimmsten Fall, was passieren kann, ist, 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, was zu beweisen, was gar nicht gilt, was einfach falsch ist.
Aber es kann nicht passieren, dass man einen halluzinierten Beweis bekomme, der dann irgendwas Falsches beweist.
Das kann dann halt einfach nicht passieren.
Nun hatten wir ja, also ich finde das gerade spannend, nun hatten wir ja irgendwie gesagt, dass letztendlich das Beweisen von Software im Wesentlichen eine Kostenfrage ist.
Hörte sich für mich jetzt jedenfalls so an oder hat gesagt, das hat eine Zeile Code und die zehn Zeilen Isabel benötigt.
Bedeutet das, dass ich durch LLAMS jetzt alle meine Software tatsächlich beweisen kann?
Also weil dann muss ich die zehn Zeilen ja nicht mehr selber schreiben.
Also so weit würde ich jetzt vielleicht noch nicht gehen.
Vielleicht können wir da noch mal 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...
Ich habe damals, Anführungszeichen, Machine Learning schon mal einiges an Zeit eingespart.
Ich habe in meinem Projekt für meine Dissertation einen Beweis drin, den ich bis heute selber nicht 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 halt geholfen, diesen Beweis tatsächlich abzuschließen, an dem ich halt irgendwie 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 vielleicht inkrementelle Fortschritte kriegen.
Und es ist halt einfach ein sehr komplexes Problem.
Also es gibt ja viele Theoreme, 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 irgendwie 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 Isabel-Code schreiben können.
Das wird wahrscheinlich auch schwierig.
bis morgen da zehn Leute zu finden.
Nee, 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 im normalen Software-Tutorial 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 Domänenobjekte klar identifiziert.
Dann hat man seine Value-Objects, die immutable sind und dann die Interaktion 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?
Na ja, 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 dem 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 Plus.
Kommt von Leslie Lamport, der vielleicht dem einen oder anderen ein Begriff ist.
Weil er LATIC gebaut hat.
Genau, und noch viele andere Sachen gemacht hat.
Und das ist nicht so 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 drüber nachgedacht, was passiert, wenn du im Zustand X bist und dann Y passiert?
Und das ist dann zwar noch kein richtiger Beweis, weil TLL Plus 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 zurück an das Whiteboard und sage, ich muss jetzt nochmal 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ütze, weil das eigentlich deine Aussage?
Richtig, genau.
Also es ist auf jeden Fall etwas, was vor der Implementierung passiert.
Ja, ich habe so eine, also 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 eigentlich davon ausgehen, dass wir halt irgendwo 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, normaler Entwicklerin irgendwie...
selber lösen sollte und ich sollte eher versuchen, dann eine Library zu benutzen, die das halt irgendwie tut.
Also zu einem gewissen Grad würde ich zustimmen.
Also 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 Consultants einkaufen, die mir das dann machen.
Aber ich glaube ehrlich gesagt, dass man viele Sachen auch lernen kann.
Also vielleicht kann man jetzt nicht Isabel 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, dann 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 soll 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 nicht.
Also du hast ganz viel über Isabel 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 Mathe-Studium mal mit reinnehmen ins Team.
Also es ist nicht so einfach, Leute zu finden, die das als im Hintergrund haben, die damit schon Erfahrung 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 Spring Boot-Lehrbücher gibt, gibt es halt auch zum Beispiel für TLA Plus Lehrbücher oder ein Bekannter von mir hat ein...
Ich arbeite gerade an einem Buch, das nennt sich Logic for Programmers.
Da stehen eben auch solche Dinge drin, wie man zum Beispiel mit Prädikatenlogik Sachen formalisieren kann.
Und das kann man sich halt mal anschauen.
Und dann ist man vielleicht nicht so super produktiv, genau wie man eine neue Programmiersprache lernt, dann nicht so super produktiv 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 anzugehen 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 Kuratoren für dieses Formate Methoden.
für den formalen Methoden-Lehrplan beim ISLQB.
Mike 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 gebaut haben mit funktionaler Programmierung.
Wir hatten, glaube ich, auch eine grundlange Episode mit ihm mit funktionaler Programmierung.
Ich erinnere mich, dass wir da zusammengesessen haben.
Und dann ist es noch die Isabella Stilkerich, wenn ich es richtig sehe.
Was machst du, was macht ihr in dieser Rolle?
Als Kuratoren von dem Lehrplan.
Ja, genau.
Also ich habe mal ganz schnell gesagt, wir haben den Lehrplan entwickelt.
Das heißt, wir haben uns an der Entwicklung des Lehrplan, es waren 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-Erford.
Wir haben also uns zusammengesetzt, 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?
haben eben ein paar Themen zusammengetragen und dann ja 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, ja okay, also 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 Schulung können Beispiele genannt werden.
Aber wir schreiben zum Beispiel jetzt nicht vor, man muss Isabel...
ein Isabel-Workshop machen oder sowas.
Das heißt, wir haben im Prinzip aus diesem Miro-Boot dann Schritt für Schritt wieder Sachen rausgestrichen und gesagt, was ist eigentlich das Minimum, was ein Softwarearchitekt oder eine Softwarearchitektin 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.
dann mein System bestimmte Korrektheitseigenschaften beweisen zu können.
Okay, also einmal die Art und Weise, wie ich die Architektur baue, um solche Methoden einsetzen zu können und dann halt einen Überblick über diese verschiedenen Methoden.
Genau, aber es ist eben ganz wichtig, dass wir hier kein, wir machen jetzt kein Tutorial für irgendeine formale Methode.
weil das natürlich auch nicht die Aufgabe originär von dem ISA-QB-Modul ist.
Also wir machen ja da keine Java-Schulung und keine Isabel-Schulung, keine Sova-Schulung.
Also es geht ja immer darum, dass man den mal aus einer hohen Flughöhe das im Überblick hat, was da alles so an Möglichkeiten besteht.
Ich glaube, da sollten wir auch noch kurz erwähnen, so ein Lehrplan ist eben ein Lehrplan.
Das heißt also, jeweiligen Anbieter dieses Moduls können den dann unterschiedlich ausführen und können sich halt irgendwie unterschiedlich überlegen, wie sie es halt umsetzen können.
Ja, also mit, du sagtest jetzt mit unterschiedlichen Werkzeugen, aber auch die Sachen auch in unterschiedlicher Reihenfolge vermitteln und so weiter und so weiter.
Und auch Übungen.
Also ich gehe davon aus, wenn man diese Schulung besucht, dass man dabei den meisten Schulungsanbietern irgendwie Prädikatenlogik zumindest mal hinschreiben sollte und mal 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 ISAQB-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.
Da gibt es auch, in ä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 der nächste 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 sowas 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 diese 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, also 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.
Weil gerade im Embedded-Bereich halt diese Geschichten sind, wo ich halt versuche, Dinge zu steuern und das ist irgendwie nicht cool, wenn ich das sozusagen falsch mache.
Genau, das ist, wie gesagt, das Flugzeug.
Das sollte möglichst nicht durch Null dividieren.
Exakt.
So, jetzt kommt, also der Nils Brodersen hat bei LinkedIn eine Frage gestellt.
Die ist, glaube ich, sozusagen nicht so ganz im Kern der Diskussion, aber mal schauen.
Also die Frage oder die Aussage ist halt, ich wage mal die These, dass Softwareentwicklung in Zukunft zu 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 AI-Solution-Architekt als Entwickler?
Also ich würde zu 80 Prozent der Frage zustimmen.
Also das strategische Denken und das tiefe Verstehen der Zusammenhänge bin ich ein großer Fan davon, nämlich erst mal.
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 das 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 einen dann die 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änzt zu dem, was du gesagt hast, ich würde das soweit 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 halt irgendwie die, wie soll ich sagen, die implizite Annahme, dass Entwickler in 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 halt mit dieser AI-Debatte habe, und das wird hier halt irgendwie auch so ein bisschen klar, oder das klingt hier ein bisschen an, ist halt diese 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 halt irgendwie diese Episode, die ich vor einiger Zeit gemacht habe von wegen Programmierung als Modellbildung, äh Quatsch, als Theoriebildung, basierend auf dem Paper von dem Peter Nauer, wo er im Prinzip sagt, dass halt 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 Kodes ist und das ist etwas, was eben bedeutet, dass ich als Entwickler nicht nur Code produziere, sondern mir, 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 InnoQ-Blog, wo halt letztendlich drin stand, also cool, dass halt AI, also ich paraphrisiere und ich hoffe, sie sieht mir das sozusagen nach, wo sie halt 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 halt tatsächlich relevant sind und nicht 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, man hat halt XY 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 nehmen wir, gibt es, produziere und das ist eben 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önnten halt sozusagen die Cell Machine wegwerfen und dadurch, dass wir darüber geredet haben, haben wir trotzdem einen Vorteil.
Und 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...
Abschlusslos werden wollen wir?
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, genau.
Absolut, ja.
Gut, dann würde ich sagen, vielen Dank.
Nochmal der Hinweis auf das ISRQB Softwarearchitekturforum am 16.
und 17.06.
und da haben wir beide Vorträge.
Wir haben auch denke ich noch, werden noch Episoden in der Vorbereitung haben und dann eben insbesondere das Pendant darüber, wie LMS denn nun das Lernen beeinflussen.
Dann bis dahin und genau, ich hätte jetzt fast gesagt, schönes Wochenende ist ein bisschen früh, also es ist doch nicht Freitag, aber weiterhin einen guten Start in die Woche wäre, glaube ich, die richtige Aussage.
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.
Tschüss.
Tschüss.
Hier ein Hinweis in eigener Sache.
Softwarearchitektur im Stream ist live vor Ort.
Wir sind beim ISAQB Software Architecture Forum 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.