Formale Verifikation durch Übersetzung der Rust-Crates core und alloc nach Coq

 (formal.land)
1 Punkte von GN⁺ 2024-05-16 | 1 Kommentare | Auf WhatsApp teilen
  • coq-of-rust, das Rust-Programme nach Coq überträgt, unterstützt nun auch die Crates core und alloc der Standardbibliothek und verringert damit den Aufwand, Coq-Definitionen für einzelne primitive Funktionen von Hand zu schreiben
  • Da beide Crates große Codebasen mit viel unsafe und fortgeschrittenem Rust-Code sind, besteht die zentrale Aufgabe darin, die automatisch übersetzten Ergebnisse in kompilier- und verifizierbaren Einheiten zu handhaben
  • Nach der Aufteilung der Ausgabe nach einzelnen Eingabe-Rust-Dateien umfasste alloc 54 Dateien mit 171.783 Zeilen und core 190 Dateien mit 592.065 Zeilen, was Parallelkompilierung und Debugging erleichterte
  • Modulnamenskonflikte in impl-Blöcken wurden durch Einbeziehung von Informationen aus der where-Klausel entschärft, dennoch bleiben derzeit 4 % der Dateien in Coq nicht kompilierbar
  • Das Beispiel Option::unwrap_or_default wird verwendet, indem die Gleichwertigkeit zwischen der automatisch übersetzten Definition und einer einfachen funktionalen Definition bewiesen wird; dafür sind sowohl Vertrauen in die Automatisierung als auch Prüfungen zum Beweiszeitpunkt nötig

Verarbeitung von Primitives in der Rust-Standardbibliothek

  • Formal Land entwickelt coq-of-rust, das Rust-Programme in das formale Beweissystem Coq übersetzt
  • Bisher musste man zur Behandlung primitiver Bestandteile der Rust-Standardbibliothek für jede Funktion separat eine Coq-Definition erstellen, die ihr Verhalten beschreibt
  • Um diesen Aufwand zu verringern, wurden die Rust-Crates core und alloc mit coq-of-rust übersetzt
  • Die Übersetzungsergebnisse sind unter folgenden Pfaden einsehbar

Ergebnisse des ersten Übersetzungslaufs

  • Beim ersten Ausführen von coq-of-rust auf alloc und core entstanden zwei Coq-Dateien mit jeweils mehreren hunderttausend Zeilen, die jeweils die gesamte Crate abdeckten
  • Damit wurde zwar bestätigt, dass das Tool auch auf großen Codebasen läuft, der erzeugte Coq-Code ließ sich jedoch nicht sofort kompilieren
  • Fehler traten selten auf, ungefähr einer alle paar tausend Zeilen
  • Laut cloc hatte der Eingabe-Rust-Code folgenden Umfang
    • alloc: 26.299 Zeilen Rust-Code
    • core: 54.192 Zeilen Rust-Code
  • Da während der Übersetzung Makroexpansion erfolgt, ist das tatsächliche Übersetzungsziel größer als die ursprüngliche Zeilenzahl

Aufteilung des erzeugten Coq-Codes

  • Die größte Änderung bestand darin, die Ausgabe von coq-of-rust so aufzuteilen, dass pro Eingabe-Rust-Datei genau eine Coq-Datei erzeugt wird
  • Das war möglich, weil die Übersetzung unempfindlich gegenüber der Reihenfolge von Definitionen ist und context-free arbeitet
  • Zwischen Rust-Dateien gibt es üblicherweise zyklische Abhängigkeiten, die Coq nicht erlaubt, doch bei dieser Übersetzungsmethode war eine Trennung auf Dateiebene möglich
  • Nach der Aufteilung hatte die Ausgabe folgenden Umfang
    • alloc: 54 Coq-Dateien, 171.783 Zeilen Coq-Code
    • core: 190 Coq-Dateien, 592.065 Zeilen Coq-Code
  • Durch die Aufteilung wurde die Navigation und Wartung des erzeugten Codes einfacher
    • Die Kompilierung lässt sich leichter parallelisieren
    • Debugging kann gezielt dateiweise erfolgen
    • Nicht kompilierbare Dateien lassen sich leichter ausklammern
    • Diffs einzelner Dateien lassen sich einfacher nachverfolgen

Behebung von Modulnamenskonflikten und verbleibende Dateien

  • Einige Bugs wurden durch Modulnamenskonflikte in impl-Blöcken verursacht
  • Die Lösung bestand darin, mehr Informationen in Modulnamen aufzunehmen, um ihre Eindeutigkeit zu erhöhen
    • Informationen aus der zuvor fehlenden where-Klausel wurden einbezogen
    • Beispielsweise spiegelt bei der Default-Trait-Implementierung für Mapping<K, V> der Modulname die Bedingung wider, dass sowohl K als auch V Default implementieren müssen
  • Aktuell lassen sich folgende Dateien in Coq nicht kompilieren
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Das entspricht 4 % aller Dateien
  • Allerdings werden auch in kompilierbaren Dateien noch nicht unterstützte Rust-Bestandteile axiomatiziert, daher lässt sich aus dieser Quote allein nicht der gesamte nicht unterstützte Bereich ableiten

Übersetzungsbeispiel Option::unwrap_or_default

  • Rusts Option::unwrap_or_default gibt bei Some(x) den Wert x zurück und ruft bei None T::default() auf
  • coq-of-rust übersetzt dies in eine monadische Coq-Definition
    • Eingabeargumente und Typen werden abgeglichen
    • Im Some-Zweig wird auf das Tupelfeld zugegriffen und dessen Wert kopiert
    • Im None-Zweig wird die default-Methode des Traits core::default::Default aufgerufen
  • Für die eigentliche Verifikation wird statt der automatisch erzeugten Definition eine einfachere funktionale Definition verwendet
    • Bei None wird core.simulations.default.Default.default zurückgegeben
    • Bei Some x wird x zurückgegeben
  • Der Beweis der Gleichwertigkeit zwischen der automatisch erzeugten und der einfachen Definition steht in CoqOfRust/core/proofs/option.v
  • Wenn sich der ursprüngliche Rust-Code ändert, wird diese Änderung über den Beweis erfasst
  • Da die Übersetzung der core-Bibliothek automatisch erfolgt ist, kann man den erzeugten Definitionen stärker vertrauen als von Hand geschriebenen Definitionen
  • Dennoch kann auch coq-of-rust Fehler oder Unvollständigkeiten enthalten, weshalb beim Beweis geprüft werden muss, ob der Code gültig ist

Verbleibende Aufgaben

  • Das Vertrauen in die Formalisierung der Standardbibliothek bei der Verifikation von Rust-Programmen steigt
  • Das nächste Ziel ist weiterhin die Vereinfachung des weiterhin mühsamen Beweisprozesses
  • Um insbesondere zu zeigen, dass eine Simulation dem ursprünglichen Rust-Code entspricht, sind folgende Arbeiten nötig
    • Namensauflösung
    • Einführung höherer Typen
    • Entfernung von Seiteneffekten
  • Diese Schritte getrennt zu behandeln, ist die Richtung für weitere Verbesserungen

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-05-16
Hacker-News-Kommentare

  • Wirklich beeindruckend
    Solche automatischen Übersetzungen verlagern das Vertrauensobjekt auf das Werkzeug. coq-of-rust selbst ist nicht in Coq, sondern in Rust geschrieben, daher ist diese rekursive Struktur ziemlich erstaunlich, aber wenn man einen CompCert-artigen Ansatz mit der Methode kombiniert, Ken Thompsons Trusting-Trust-Angriff mit einem zweiten Compiler zu umgehen, wie in David A. Wheelers „Countering Trusting Trust through Diverse Double-Compiling“ (2009) [0], dann scheint ein Korrektheitsbeweis möglich zu sein
    Zur Verifikation könnte man den coq-of-rust-Übersetzer mit coq-of-rust von Rust nach Coq übersetzen, und auch wenn diese Übersetzung in Rust durchgeführt wurde und man ihr daher nicht unbedingt vertrauen muss, kann man innerhalb von Coq die gewünschten Korrektheitseigenschaften beweisen, insbesondere dass bei der Übersetzung von Rust-Programmen nach Coq die Semantik erhalten bleibt
    Wahrscheinlich ist es einfacher, mit Definitionen zu beweisen, die funktionaler sind als die im Paper erzeugten Definitionen; dann kann man wie in der Standardbibliothek die Äquivalenz zwischen den Definitionen beweisen. Wenn der coq-of-rust-Übersetzer, insbesondere lib/ [1], derzeit 6.350 Zeilen Rust umfasst, erscheint es auch realistisch, den gesamten Übersetzer in Coq zu schreiben und die Äquivalenz mit dem erzeugten Ergebnis zu beweisen
    Führt man dann den bewiesenen Coq-coq-of-rust-Übersetzer auf den in Rust geschriebenen coq-of-rust-Quellcode aus, sollten die ausgegebenen Coq-Definitionen mit der Ausgabe des ursprünglich verwendeten, in Rust geschriebenen coq-of-rust-Übersetzers übereinstimmen
    Nebenbei ist es schön zu sehen, dass es für solche Arbeiten Industriefinanzierung gibt. Ich bin Kryptowährungen gegenüber eher zynisch, aber es stimmt, dass die dortigen Korrektheitsanforderungen Verbesserungen in meinen Interessengebieten vorantreiben, etwa bei Rust, Coq und der Unterstützung informierter Masterstudierender
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Ich bin einer der Autoren, und tatsächlich könnte ein solches Verfahren ein guter Weg sein, coq-of-rust zu verifizieren
      Allerdings hängt das Parsen und Typprüfen des eingegebenen Rust-Codes trotz des kurzen Codes selbst vom Rust-Compiler ab. Diesen Teil müsste man also ebenfalls verifizieren oder zumindest ohne Beweis formal spezifizieren. Ein Hindernis ist, dass die rustc-API ziemlich groß und instabil ist, aber es könnte dennoch ein Weg sein, das Vertrauen zu erhöhen
    • Das erinnert mich an die Zeit, als ich früher mit SPARK Ada gearbeitet habe. Bei Projekten ohne unterstütztes Ada-Ziel, insbesondere auf sehr kleinen Geräten, haben wir Ada in C übersetzt und es dann für das jeweilige Ziel kompiliert, wodurch auf der SPARK-Seite verschiedene Formen statischer Analyse möglich wurden
      Natürlich entstand damit das Problem, das Ausgabeartefakt oder den Übersetzer zu verifizieren, aber der resultierende C-Code war für Verifikationszwecke recht gut lesbar und stilistisch eingeschränkt, und auch das Vertrauen in die Werkzeuge war hoch. Die statische SPARK-Analyse war nur ein Teil des gesamten Verifikations- und Validierungsprozesses, und Tests sowie andere Aktivitäten lieferten zusätzliche Vertrauensebenen. Insgesamt war das ein Ansatz, der ziemlich gut funktionierte
    • Dass Kryptowährungen so etwas fördern, liegt nicht nur an Korrektheitsanforderungen, sondern auch daran, dass viel überschüssiges Vermögen an Menschen mit Interesse an Informatik geflossen ist
      Dass sie dieses Geld für Informatikforschung ausgeben, ist nicht nur in ihrem Eigeninteresse, sondern auch eine Form von Wohltätigkeit, die an ihr Hobby anschließt
    • Ich verstehe nicht ganz, wie dieser Ansatz verhindert, dass der Rust-Compiler, der zur Erzeugung der Binärdatei verwendet wird, eine bösartige Payload einschleust. Man könnte A mit B bauen und B mit A und anschließend die Binärdateien vergleichen
      Ein anderer Ansatz wäre Proof-Carrying Code. Der Rust-Compiler würde dann zusammen mit der ausführbaren Datei einen Coq-Beweis ausgeben, dass die Ausgabe semantisch dem eingegebenen Quellcode entspricht
      Natürlich könnte man auch einen Compiler für eine Teilmenge von Rust schreiben, etwa ohne Borrow Checker oder Optimierungen und direkt in Maschinencode für eine bestimmte Architektur, und von dort aus alles bootstrappen

  • Die Größe von Programmen, die sich mit einem halbautomatischen deduktiven Beweissystem wie Coq von Anfang bis Ende verifizieren lassen, ist klein. Bibliotheken könnten einfacher sein, weil der Grad der Interaktion zwischen Codeteilen geringer ist, aber allgemeine Programme sind das nicht
    Tatsächlich ist das Wachstum der Programmgröße, die sich auf diese Weise verifizieren lässt, langsamer verlaufen als das Wachstum der durchschnittlichen Gesamtgröße von Programmen. Solide Softwareverifikation, also der Nachweis einer 100%igen Übereinstimmung mit der Spezifikation, ist klar nützlich, etwa beim Korrektheitsbeweis von Kernalgorithmen, skaliert aber nicht gut
    Deshalb ist die Forschung teilweise zu unsoliden Methoden übergegangen. Die Kosten einer 100%-Garantie können zehnmal so hoch sein wie die einer 99,9999%-Garantie, und der Unterschied in der Fehlerwahrscheinlichkeit kann kleiner sein als die Ausfallwahrscheinlichkeit außerhalb der Software. Bei physischen Systemen kann man von vornherein nicht beweisen, dass sie der Spezifikation entsprechen, und es besteht auch eine gewisse Wahrscheinlichkeit, dass die Spezifikation selbst nicht ausreichend zur Realität passt

    • Der entscheidende Punkt ist, dass man, wenn man die unsafe-Teile der Standardbibliothek und die Sicherheitsgarantien von Rust beweist, transitiv die Speichersicherheit, die Abwesenheit von Data Races usw. für allen sicheren Rust-Code beweisen kann, der nur die Standardbibliothek verwendet
      Nur die Korrektheit von unsafe-Code zu beweisen ist mit weit weniger Aufwand möglich, als sämtlichen Rust-Code zu beweisen. Das ist eine Antwort auf die häufige Kritik „Aber was ist mit unsafe-Code?“, die bei Rusts Sicherheitsgarantien oft aufkommt. Lücken, für die das Rust-Typsystem allein nicht stark genug ist, kann man mit stärkeren Systemen wie Coq schließen

  • An solchen Versuchen gibt es einen Punkt, den ich nicht ganz verstehe. Wenn der Code manuell oder halbautomatisch nach Coq übertragen werden muss, ist dann nicht die Wahrscheinlichkeit von Fehlern in diesem Prozess viel größer als der Nutzen, den man durch formale Verifikation gewinnt?
    Anders gesagt: Woher wissen wir, dass das, was wir bewiesen haben, weiterhin für den Originalcode gilt?

    • Das wissen wir nicht. Am Ende muss man irgendetwas vertrauen: der Hardware, dem Compiler, der Spezifikation, dem Trusted Kernel von Coq usw.
      Über formale Verifikation wird oft so gesprochen, als beseitige sie die Möglichkeit von Bugs vollständig, tatsächlich geht es aber eher darum, die Wahrscheinlichkeit von Bugs stark zu senken. Trotzdem ist eine automatische Übersetzung zwischen Rust und Coq einer manuellen Übersetzung vorzuziehen, weil sie die Komplexität dessen, was man vertrauen muss, erheblich reduziert.
    • Das ist zwar eine echte Grenze, aber keine besonders schlimme.
      In vielen Fällen führen Bugs in der Übersetzung einfach dazu, dass ein Beweis nicht möglich ist. Dann untersucht jemand, warum der Beweis nicht durchgeht, und findet dabei den Übersetzungsfehler.
      Das eigentliche Problem ist der Fall, dass ein Bug in der Übersetzung einen Bug im Originalcode exakt ausgleicht. Wenn kein systematisches Risiko vorliegt, ist es ziemlich unwahrscheinlich, dass sich zwei Bugs auf diese Weise gegenseitig aufheben.
    • Der Code wird mit coq-of-rust automatisch übersetzt. Wenn in der Übersetzung ein Problem gefunden wird, muss man es einmal im Tool coq-of-rust beheben, und alle Übersetzungsergebnisse werden aktualisiert.

  • Für interessierte Leser: Ich habe diesen Blogpost eingereicht, weil er weniger direkt mit Kryptowährungen zu tun hat als andere Beiträge in demselben Blog, dort gibt es aber viele technisch interessantere Texte.
    Besonders die beiden neuesten Beiträge behandeln, wie derselbe Ansatz nicht auf Rust, sondern auf Python angewendet wird.

  • Ich musste an einen Vortrag [1] denken, in dem ein Fuzzer Bugs in einem formal verifizierten C-Compiler fand. Das lag daran, dass die formale Verifikation Frontend und Backend nicht einschloss.
    Mir ist auch klar, dass die Frage aufkommt, wie sehr man Coq selbst oder der Übersetzung vertrauen kann, und ich frage mich ebenfalls, wie das mit Rust-Updates synchronisiert werden soll, aber selbst perfekte formale Verifikation bedeutet nicht von Anfang bis Ende 100%ige Korrektheit.
    [1] https://youtu.be/Ux0YnVEaI6A

  • Ich bin überhaupt kein Experte für formale Verifikation, aber wenn die Standardbibliothek von Rust formal verifiziert wäre und keinen unsafe-Code verwenden würde, hätten dann alle Rust-Programme, die diese formal verifizierte Bibliothek benutzen, in Bezug auf Speicherbehandlung praktisch formal verifizierte Qualität?

    • Rusts Sicherheit hat fast nichts mit Bugfreiheit zu tun.
      Rust hat eine eigene Definition von „safe“, und die kann man als Teilmenge von Speichersicherheit sehen. Selbst in vollständig sicherem Rust-Code sind Data Races, Deadlocks, Speichererschöpfung usw. möglich, von logischen Fehlern ganz zu schweigen.
    • In gewissem Maß ist das wohl der Traum, aber es gibt viele Vorbehalte, und einige Dinge müssten zusammenpassen.
      Erstens müsste man die Semantik von unsafe Rust formalisieren. Die wegweisende RustBelt-Arbeit[1] von Ralf Jung war ein großer Fortschritt, ist aber noch nicht vollständig. Insbesondere erweist sich Pointer Provenance als schwieriger Faktor.
      Zweitens braucht man als Teil davon ein formales Modell des Borrow-Checkers. Stacked borrows[2] war ein guter Versuch, hat aber Mängel, und Tree borrows[3] könnte das beheben, wobei auch etwas noch Ausgefeilteres möglich ist.
      Drittens braucht man ein formales Speichermodell. Das betrifft vor allem das Verhalten atomarer Operationen und von Synchronisation und ist daher für Standardbibliothekskomponenten wie Arc sehr wichtig. Dass Rusts Speichermodell dem von C++ ähneln und damit interoperabel sein sollte, wird weithin akzeptiert, aber Probleme wie „out of thin air“ und fehlende Features wie seqlock bleiben offen. Das ist einer der Gründe, warum der Linux-Kernel weiterhin sein eigenes Modell verwendet.
      Viertens braucht man einen Beweis dafür, dass sich Sicherheitsgarantien gut komponieren lassen. Insbesondere muss die Sicherheitsgarantie erhalten bleiben, wenn korrekter Code in unsafe Rust mit safe-Rust-Code kombiniert wird. Bisher gibt es gute Ergebnisse, aber das muss für das Gesamtsystem bewiesen werden.
      Fünftens müsste man alle verbleibenden Soundness-Bugs in Rust[1] schließen, damit ein solcher Beweis für allen Code gilt. Viele dieser Probleme sind eher theoretisch oder werden erst bei gegnerischem Code[5] praktisch relevant, weshalb der Fortschritt langsam ist.
      Selbst wenn all das geschafft ist, bleiben es nur partielle Garantien. Ein riesiger Teil der Schnittstellen zur Außenwelt basiert auf unsafe-Code. Solange man nur rein rechnet, mag das anders sein, aber wenn man zum Beispiel eine grafische UI baut, kann immer noch sehr viel schiefgehen.
      Trotzdem gibt es einen praktischen Weg nach vorn, und der würde zu einer Lage führen, die deutlich besser ist als der heutige allgemeine Zustand voller verwundbarer Systeme.
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Ich bin kein Rust-Experte, aber im core-Code scheint es ziemlich viel unsafe zu geben. Das ist auch nachvollziehbar.
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Ich glaube nicht, dass Coq in dem hier vorgestellten Ansatz alle unsafe-Aufrufe verifizieren kann.

  • Kann man vergleichen, wie sich dieser Ansatz von Aeneas oder RustHornBelt unterscheidet? Wie werden Pointer und veränderliche Borrows behandelt?

    • Ich weiß nicht, wie RustHornBelt funktioniert. Wir konzentrieren uns auf sicheren Code, erzeugen aber auch für unsafe-Blöcke nach bestem Bemühen eine Übersetzung.
      Im Vergleich zu Aeneas ist das Ziel sehr ähnlich. Beide wollen Rust-Programme mit einem interaktiven Theorembeweiser verifizieren. Bei coq-of-rust wird jedoch die reine funktionale Version des Codes, die Gegenstand des Beweises ist, von Hand geschrieben oder bei repetitiver Arbeit mit Hilfe von GitHub Copilot erstellt, und anschließend wird bewiesen, dass sie zur automatisch erzeugten Übersetzung äquivalent ist. Aeneas zielt darauf ab, die funktionale Version direkt zu erzeugen.
      Pointer werden alle als veränderliche Pointer behandelt, also als Typ *. Die Informationen des Borrow-Checkers von Rust werden nicht verwendet; das vereinfacht die Übersetzung, hat aber den Preis, dass die Last auf den Zeitpunkt des Beweises verlagert wird.
      Um Pointer im Beweis herzuleiten, müssen Nutzer einen angepassten Allocator bereitstellen, den sie danach entwerfen können, wie der Speicher verwendet werden soll. Wenn ein Programm zum Beispiel drei globale veränderliche Variablen benutzt, kann der Speicher als Record mit drei Feldern modelliert werden. Diese Felder sind anfangs None, um den Zustand „noch nicht allokiert“ darzustellen.
      Wie gut sich diese Technik skalieren lässt, wissen wir noch nicht, aber zumindest im Moment kann man damit Schlussfolgerungen mit Separation Logic vermeiden. Wir erwarten, dass die meisten Programme, die man verifizieren möchte, insbesondere auf der Anwendungsseite, eine vergleichsweise „einfache“ Speicherdiszplin haben.

  • Ist das Schreiben einer Spezifikation für formale Verifikation ähnlich wie der Einsatz komplexerer Property-based Tests? Sobald man über nicht allzu komplexe Programme hinausgeht, ist auch das Schreiben von Property-based Tests ziemlich schwierig und zeitaufwendig.

    • Ähnlich, aber nicht immer gleich. Bei Property-based Tests legt man normalerweise auf Ebene der Systemschnittstelle, auf Funktions- oder Prozedurebene oder darüber eine Beschreibung der Eingaben fest und testet, ob die Ausgaben eine bestimmte Eigenschaft oder eine Menge von Eigenschaften erfüllen.
      Wenn man formale Verifikation auf derselben Ebene macht, kann das ziemlich ähnlich aussehen. Formale Verifikationswerkzeuge können aber tiefer gehen. Man kann zum Beispiel Fragen beantworten wie: „Es gibt diese Schleifeninvariante über den Systemzustand innerhalb der Berechnung — kann bewiesen werden, dass sie in jeder Iteration tatsächlich erhalten bleibt?“ oder „Kann bewiesen werden, dass bei keiner Zwischenberechnung in diesem Ablauf jemals ein Underflow oder Overflow auftritt?“
      Ersteres ist auch mit Property-based Tests möglich, wenn man den Kern der Schleife in eine separate Prozedur auslagert und die Invariante mit vielen Zwischenzuständen testet. Letzteres ist deutlich schwieriger, außer man zerlegt das Programm so stark, dass es praktisch zeilenweise separat ausführbar wird.

  • Ich wusste nicht einmal, dass so etwas möglich ist.
    Ich frage mich, ob solche Versuche die Rust-Einführung in zentralen Teilen der Kernel-Übernahme beschleunigen könnten.

  • Kann jemand das Konzept der „Verifikation“ sehr einfach erklären? Ich frage mich, warum eigens zu diesem Zweck eine ganze Sprache wie Coq existiert und welche konkrete Bedeutung das für die Gesellschaft insgesamt hat.