Stellen Sie sich die Welt des Computings als eine riesige, geschäftige Stadt vor. Jahrzehntelang konzentrierten sich die Architekten dieser Stadt darauf, einzelne Gebäude zu entwerfen: das perfekte Haus (ein einzelnes Programm) oder die ideale Fabrik (einen einzelnen Algorithmus). Sie hatten Blaupausen dafür, wie ein einzelner Raum funktioniert oder wie eine einzelne Maschine eine einzige Aufgabe verarbeitet. Doch als die Stadt wuchs, wurde klar, dass die wahre Magie – und das wahre Chaos – in den Verbindungen zwischen den Gebäuden liegt. Wie spricht das Kraftwerk mit der U-Bahn? Wie koordiniert das Krankenhaus die Ampeln? Dies ist der Bereich des „High-Level-Computings“, in dem es nicht nur darum geht, ein einzelnes Gerät zu bauen, sondern zu verstehen, wie eine ganze Sammlung von ihnen interagiert, um komplexe Probleme zu lösen.

Um dies zu bewältigen, haben Wissenschaftler versucht, eine universelle Sprache für diese Interaktionen zu schaffen, ganz so, wie ein Stadtplaner eine standardisierte Menge an Symbolen für Straßen und Brücken verwendet. Die meisten dieser Sprachen haben jedoch einen blinden Fleck. Sie sind großartig darin, Daten zu verfolgen (die Pakete, die ausgeliefert werden), aber schrecklich darin, die Steuerung (die Verkehrssignale, die den Lastwagen sagen, wann sie fahren sollen) zu verfolgen. Einige Sprachen setzen voraus, dass die Daten der Steuerung einfach magisch folgen, während andere die Verkehrssignale gänzlich ignorieren. Dies macht es unglaublich schwierig vorherzusagen, was passiert, wenn man zwei komplexe Systeme miteinander verbindet. Man landet unter Umständen in einem Stau, in dem die Lastwagen auf ein Signal warten, das niemals kommt, oder in einem Zusammenstoß, bei dem zwei Signale versuchen, denselben Lastwagen gleichzeitig zu dirigieren. Die große Frage lautet: Können wir ein System bauen, das die „Verkehrssignale“ (Steuerung) und die „Pakete“ (Daten) als getrennte, aber verbundene Dinge behandelt, damit wir komplexe, zuverlässige Systeme ohne das Chaos aufbauen können?

Dieses Papier mit dem Titel „Colimit-Based Composition of High-Level Computing Devices“ von Damian Arellanes tritt in dieses chaotische Schnittfeld ein, um einen neuen, saubereren Weg zum Bau dieser digitalen Städte anzubieten. Der Autor führt eine verfeinerte Version eines Modells namens „Computon“ ein. Betrachten Sie einen Computon als einen modularen Lego-Stein, aber anstatt nur nach Form zusammenzuklicken, klicken diese Steine basierend auf strengen Regeln zusammen, wer mit wem und wann kommuniziert. Das Paper stellt fest, dass durch die Verwendung eines speziellen mathematischen Werkzeugs namens „Colimit“ (was eine Art hochpräzises Zusammenkleben ist), wir ein System schaffen können, in dem Steuersignale und Daten in getrennten Fahrspuren gehalten werden, aber dennoch perfekt zusammenarbeiten.

Das Paper kritisiert explizit spezifische bestehende Modelle, insbesondere zustands- und datenorientierte Modelle, da sie den Kontrollfluss vernachlässigen, anstatt die Möglichkeit flexibler Formalismen im Allgemeinen abzulehnen. Es argumentiert, dass das Vermischen von Daten und Steuerung innerhalb desselben Frameworks zu ineffizienten Methoden für die formale Analyse führt. Stattdessen schlägt der Autor vor, dass wir durch die Trennung von „Verkehrslichtern“ und „Fracht“ komplexe Maschinen mit partiellen Typ-Ebene-Garantien und struktureller Korrektheit durch Konstruktion bauen können. Das bedeutet, das System ist so konzipiert, dass das resultierende Gefüge garantiert korrekt ist, wenn man die Montagevorschriften befolgt, obwohl es nicht behauptet, jedes mögliche Laufzeitverhalten absolut zu beweisen. Das Paper schlägt nicht nur vor, dass dies eine gute Idee ist; es baut tatsächlich einen funktionierenden Prototyp. Die Autoren haben diese gesamte Theorie in einer Programmiersprache namens Idris 2 implementiert, wodurch ein echtes, Open-Source-Werkzeug entstanden ist, mit dem Menschen diese komplexen Rechengeräte bauen können. Sie zeigten, dass dieses Werkzeug sequentielle Schritte (nacheinander), parallele Schritte (gleichzeitig) und Verzweigungen (Wahl zwischen verschiedenen Pfaden) handhaben kann, während der Kontrollfluss explizit und fehlerfrei bleibt.

Um zu verstehen, wie das funktioniert, stellen Sie sich vor, Sie bauen einen riesigen, automatisierten Sandwich-Laden. In den alten Modellen waren die Anweisungen für „Leg das Brot auf den Tisch“ und „Greif nach dem Schinken“ auf demselben Blatt Papier geschrieben, vermischt mit dem Rezept für die Sauce. Wenn Sie versuchten, zwei verschiedene Sandwich-Läden zu kombinieren, würden sich die Anweisungen kreuzen, und Sie könnten am Ende Schinken auf dem Boden oder Brot im Toaster haben.

In dem neuen „Computon“-Modell, das im Paper beschrieben wird, sind die Anweisungen in zwei distinkte Systeme aufgeteilt. Sie haben das Steuerungssystem (die Verkehrssignale) und das Datensystem (die Zutaten).

• Das Steuerungssystem ist wie eine Gruppe von Ampeln und Walkie-Talkies. Es transportiert keinen Schinken oder Käse; es transportiert nur die „Go“-Signale. Es sagt: „Okay, das Brot ist bereit, schicke jetzt den Schinken!“ oder „Stopp! Warte auf den Salat!“
• Das Datensystem ist das Förderband, das die eigentlichen Zutaten trägt. Es bewegt sich nur, wenn das Steuerungssystem ihr grünes Licht gibt.

Das Paper führt einen speziellen „Kleber“ ein (mathematisch als „Colimit“ bezeichnet), der es Ihnen ermöglicht, diese Systeme zusammenzustecken.

• Sequenzierung: Sie können zwei Maschinen so zusammenstecken, dass die zweite erst startet, wenn die erste fertig ist. Es ist wie ein Staffellauf, bei dem der Stab (das Steuersignal) übergeben werden muss, bevor der nächste Läufer starten kann.
• Parallelisierung: Sie können zwei Maschinen nebeneinander platzieren. Beide starten zur gleichen Zeit, aber sie haben ihre eigenen separaten Verkehrssignale. Sie stoßen nicht zusammen, weil ihre Steuersignale getrennt gehalten werden.
• Verzweigung: Das ist der spannendste Teil. Stellen Sie sich eine Weggabelung vor, an der das Verkehrssignal entscheidet, ob es die Zutaten zur „Schinken-Sandwich“-Station oder zur „Käse-Sandwich“-Station schickt. Das Paper führt eine neue Art vor, diese Gabelungen zu bauen, die flexibler ist als zuvor, indem sie „offene“ Entscheidungen erlaubt, bei denen die Ausgänge nicht perfekt übereinstimmen müssen, oder „geschlossene“ Entscheidungen, bei denen alles fest verschlossen ist.

Die Autoren haben diese Ideen nicht nur auf ein Whiteboard gezeichnet; sie haben eine echte digitale Werkstatt gebaut. Sie haben ein Computerprogramm (unter Verwendung einer Sprache namens Idris 2) geschrieben, das als Sicherheitsinspektor fungiert. Wenn Sie versuchen, zwei Computons auf eine Weise zusammenzustecken, die gegen die Regeln verstößt (wie etwa, ein Verkehrssignal an ein Förderband zu koppeln, das gar nicht existiert), stoppt Sie das Programm sofort. Es ist, als hätte man ein Lego-Set, bei dem die Teile physisch nicht zusammengesteckt werden können, wenn sie nicht in das Design passen.

Das Paper behebt auch einige Fehler der ursprünglichen Theorie. Beispielsweise zeigten sie, dass man nicht tatsächlich eine spezielle, komplizierte Maschine benötigt, um Dinge zur exakt gleichen Zeit geschehen zu lassen (synchrone Parallelisierung). Man kann dieses Verhalten bauen, indem man einfach ein „Warte“-Signal und ein „Geh“-Signal hintereinander schaltet. Sie haben auch bewiesen, dass es eine „Tu-nichts“-Maschine (einen Unit-Computon) gibt, die wie ein perfekter neutraler Partner fungiert; wenn man sie an seine Maschine ankoppelt, verändert sich die eigene Maschine überhaupt nicht, was eine entscheidende Eigenschaft beim Bau komplexer Systeme aus kleineren Teilen ist.

Letztendlich bietet dieses Paper ein Werkzeugset für die Zukunft des Computings. Es bietet einen Weg, massive, interagierende Systeme – wie ein Netzwerk für selbstfahrende Autos oder eine globale medizinische Datenbank – zu konstruieren, indem man kleine, verifizierte Blöcke zusammensteckt. Da der Kontrollfluss explizit und von den Daten getrennt ist, können wir viel sicherer sein, dass diese Systeme nicht abstürzen oder verwirrt werden. Die Autoren sehen eine Zukunft voraus, in der Entwickler vorgefertigte, zertifizierte „Computons“ aus einer digitalen Bibliothek wählen und diese zusammenstecken können, um neue Anwendungen zu erstellen, in dem Wissen, dass die Verkehrssignale immer korrekt funktionieren werden, egal wie groß die Stadt auch wird. Es ist ein Übergang von der Hoffnung, dass unsere komplexen Systeme funktionieren, hin zu der mathematischen Garantie, dass sie es tun.