Guter Artikel. Aus der Perspektive von jemandem, der früher Programmverifikation betrieben hat, wirkt Rust wie die nützlichste moderne Sprache für die Anwendung formaler Methoden.
Rusts Regeln beseitigen viele Fälle, die schwer zu formalisieren sind. Das verbleibende große Problem ist die Deadlock-Analyse aus Thread-Sicht und aus Rc-/Borrowing-Sicht; die beiden sind bis zu einem gewissen Grad äquivalent. Wenn Rust eine statische Deadlock-Analyse hätte, würden wohl auch sichere dereferenzierbare Pointer möglich, und wenn man beweisen könnte, dass alle borrow-/upgrade-Aufrufe nicht fehlschlagen, ließe sich der Großteil des Reference Counting entfernen. Dann bekäme man, wo möglich, interne Veränderlichkeit praktisch kostenlos dazu.
Das große Problem von Theorem Provers ist, dass sie von Leuten gebaut werden, die gern Theoreme beweisen; dadurch verlieren sie sich im Formalismus, und ihr Gespür für Programmierer und UI passt nicht zusammen. Die meisten Beweispflichten lassen sich mit SAT-Solvern erledigen, aber für schwierige Probleme braucht man schwergewichtigere Werkzeuge. Coq ist zu manuell, und der Autor hält ACL2 für zu funktional. Machine Learning kann bei der Richtungsweisung für Theorem Provers helfen. Den Beweis selbst ihm zu überlassen ist schwierig, aber aus Code, dessen Control Flow und Datennutzung weitgehend ähnlich sind, Beweispläne abzuleiten, scheint machbar.
F* kommt einer sagenhaften Sprache nahe, die Beweise automatisch führt. Es nutzt SMT-Solver, die stärker als SAT sind, und wenn das automatische Lösen scheitert, sind auch manuelle Beweise möglich.
Die Kryptoroutinen von Firefox und Wireguard wurden nicht in Rust geschrieben, sondern in F*, genauer gesagt in Low*, einem in F* eingebetteten Low-Level-DSL, und sind vollständig verifiziert. https://project-everest.github.io/ https://mitls.org/
Zustimmung, aber ich denke, Lean macht dank seiner umfangreichen Metaprogramming-Funktionen große Fortschritte bei der User Experience der interaktiven Theorem-Proving-Verifikation.
Das Problem bei der Anwendung solcher Tools auf die Verifikation externer Sprachen wie Rust ist, dass die Beweise nicht in der Zielsprache geschrieben werden und Entwickler daher zwei Sprachen lernen müssen. Aufgrund meiner Erfahrung mit Creusot, Arbeiten an Verus und Aeneas sowie Erfahrungen im Why3-Labor habe ich darüber nachgedacht, wie ein „verifikationsbewusstes Rust“ aussehen könnte. Wenn man eine solche Sprache von Anfang an entwirft, könnte ihre Verifizierbarkeit gegenüber Rust schrittweise deutlich besser werden, besonders an den schwierigen Stellen von Beweisen.
Ich glaube, die Coq/Agda/Lean-Familie wird im Beweisbereich gewinnen. Interaktion ist als Feedback-Loop ein ziemlich gutes Modell, und es sind Systeme, die bereits existieren und tatsächlich funktionieren.
Was mir als eingebaute Funktion am meisten fehlt, ist etwas im Sinne von „lass quickcheck über meinen Beweis laufen“. Wenn man Code hat und versucht, eine Eigenschaft zu beweisen, die gar nicht wahr ist, kann man sich leicht die Haare raufen, weil man nicht versteht, warum der Beweis nicht klappt. Wenn man mitten im Beweis in einem unsinnigen Zustand landet, wäre es schön, wenn ein Befehl wie „erzeuge hier ein Gegenbeispiel“ ein Gegenbeispiel ausspucken würde. Beweise sind stark pfadabhängig und im Allgemeinen nicht einfach, aber diese Tools wirken sehr nah an Größe. Der Versuch, Code zu beweisen, muss auch die Möglichkeit widerspiegeln, dass dieser Code Bugs haben kann.
Die Idee, Machine Learning zur Führung von Theorem Provers einzusetzen, ist interessant. Wenn ein Machine-Learning-System richtigliegt, führt es zu einem gültigen Beweis und bringt großen Gewinn; wenn es falschliegt, entsteht kein großer Schaden.
Der Prover leitet keinen falschen Beweis ab, sondern scheitert einfach daran, einen gültigen Beweis abzuleiten. Ich denke, es gibt nicht viele Machine-Learning-Anwendungen mit dieser Eigenschaft.
Ich bin kein Experte für formale Verifikation, aber Locks im traditionellen Sinne halte ich nicht für besonders hilfreich. Kein Compiler liefert in Bezug auf Locks wirklich Brauchbares, man muss das Risiko einfach akzeptieren und damit leben.
Tatsächlich sind Locks und Reference Counts in Rust Laufzeitstrukturen. Arc bricht Rusts RAII-Modell erheblich, sodass scoped threads, deren Destruktor vor dem Ende des Scopes ausgeführt werden musste, entfernt werden mussten. Globale Reference Counts haben Probleme mit Zyklen und Leaks und werden wieder zu einem globalen Problem. Ganz wird man sie schwer los, aber ich glaube, es ist besser, sie in Arena-artige Scopes einzuschließen. Für Locks scheinen asymmetrische Datenstrukturen wie Channels nötig zu sein. In Go kann man Channels in Sender und Empfänger aufteilen und im sendenden goroutine defer close(ch) setzen; selbst bei einer Panic ist garantiert, dass es ausgeführt wird, wenn der Rest des Threads endet. Es müssen nicht unbedingt Channels sein, aber wenn man Lese-/Schreib- bzw. Producer-/Consumer-Rollen trennt, wird das Schlussfolgern viel einfacher und dürfte auch der formalen Analyse helfen.
Mir gefällt, dass es mit einem Zitat aus Hoares Paper von etwa 1973 begann und nun schon bis zu einem zweiten Artikel weitergeführt wurde. Ursprünglich hatte ich im HN-Thread zu boats Artikel einen langen Kommentar geschrieben und gesagt, dass es angesichts von boats Hintergrund zwar verständlich ist, dieses Zitat in eine Rust-zentrierte Perspektive zu kippen, dass dadurch aber der Umfang von Hoares Kritik künstlich verengt wird.
Nun hat Grayson dieses schmale Stück als Ausgangspunkt genommen, um einige interessante Bereiche und Designpunkte von Rust zu diskutieren. Ich halte meinen Kommentar weiterhin für richtig, aber die Diskussion, die sich aus Graysons Artikel ergeben hat, war ausreichend, um die technischen Einwände gegen den Ausgangsartikel aufzuwiegen.
Spätestens Mitte der 1990er Jahre hatte Hoare selbst bereits erkannt, dass an den Grundlagen des soundness-zentrierten Ansatzes der 1970er Jahre etwas falsch sein könnte: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Seitdem sind unsolide Verfahren entstanden, die über einfaches Testen hinausgehen, und meiner Ansicht nach sind unsolide Methoden den soliden inzwischen voraus.
1973 liegt 50 Jahre zurück, also ein ganzes Berufsleben eines Experten. Hoare war wirklich nah dran.
Er hatte das Problem gefunden, und rückblickend wirkt die Lösung, shared XOR mutable per Typsystem zu erzwingen, wie ein kleiner Schritt. Hätte man damals erkannt, dass genau dieser kleine Schritt die Lösung ist, hätte das 50 Jahre enormen Schmerz erspart.
Meine ursprünglichen Gedanken zu boats Hoare-Zitat waren diese: Nach Hoares erstem Zitat und einer kurzen Einleitung sagt der Autor: „Als Tony Hoare sagte, Referenzen seien wie Sprünge, behandelte er das Problem von veränderlichem, aliasbehaftetem Zustand.“ Da withoutboats ein bekannter Rust-Entwickler ist, überrascht diese Interpretation nicht.
Aber das Zitat selbst scheint diese Sichtweise nicht zu stützen. Man kann es als Versuch sehen, Hoares allgemeinere Klage über die semantische Existenz von Referenzen an sich zu nehmen und auf Rusts Modell von nicht-aliasbehaftetem veränderlichem Zustand anzuwenden, um das Problem zu umgehen. Allerdings kommt das eher dem gleich, nur ein schmales Stück eines größeren Problems zu reparieren und dann zu sagen, das ganze Problem sei verschwunden. Die ausgelassenen Teile, insbesondere der Beginn des Abschnitts „Variables“ und das ALGOL-68-Beispiel, sprechen viel stärker dafür, dass Hoare nicht nur veränderlichen Zustand kritisierte, sondern das semantische Konzept von Referenzen an sich. Ich erkenne an, dass Rust versucht, einen Teil des Problems zu zähmen, aber ich sehe keine Sprache, die dieses Problem „behoben“ hätte.
Ich verstehe nicht ganz, warum dieser Artikel so viel Lob bekommt. Es wirkt, als würden mehrere Bereiche der Programmanalyse in einem einzigen Absatz abgehandelt. Ich mag Graydon und respektiere seine Perspektive, aber dieser Absatz ist übermäßig vereinfacht.
Die Erklärung, Sprachen mit GC hätten sich nicht die Mühe gemacht, starke Unterstützung für lokales Schlussfolgern bereitzustellen, ist ein Strohmann. Es gab Sprachen wie Pony, die Regionen im Typsystem haben und trotzdem GC verwenden. Außerdem gibt es ganze Gebiete der Pointer-Analyse und Escape-Analyse, die Eindeutigkeit inferieren und bestimmen, ob zwei Referenzen Aliasse sein können. Auch der Kern statischer Typisierung besteht darin, den Heap mithilfe der Techniken Klassen und Felder in nicht miteinander aliasbehaftete Teile aufzuteilen. Es geht hier nicht um JavaScript, und man sollte nicht so tun, als gäbe es in Java/C#/Scala und zahllosen GC-Sprachen kein lokales Schlussfolgern über veränderlichen Zustand.
Im allgemeinen Fall kann man das nicht vollständig automatisch erledigen; in der Praxis braucht man etwas, das Separation Logic ziemlich ähnlich ist. Auch die Semantik des Borrow Checkers von Rust kann man als eine Art vereinfachte Separation Logic betrachten.
Klassen und Felder bieten kein vollständiges lokales Schlussfolgern über veränderlichen Zustand. Denn Klasse/Objekt A kann vom veränderlichen Zustand von Klasse/Objekt B abhängig werden. Java-artige Klassenvererbung fügt von sich aus zusätzliche Komplexität hinzu, während ein Programm im Laufe der Zeit evolviert.
Graydon hat nicht gesagt, dass GC starkes lokales Schlussfolgern unmöglich macht. Er sagt, dass die meisten Sprachdesigner aus welchen Gründen auch immer Entscheidungen getroffen haben, die diesem Ziel entgegenstehen, und das scheint offensichtlich wahr zu sein.
Gegenbeispiele gibt es natürlich, aber wenn man sich Mainstream-GC-Allzwecksprachen wie Java, C# und Python ansieht, stimmt die Aussage. Man kann die ursprüngliche Idee der Objektorientierung so interpretieren, dass sie dem heutigen Actor Model näherstand und dass man besessene Datenstrukturen nur per Message Passing verändern wollte. Die tatsächlichen Implementierungen von Objektorientierung kommen diesem Ziel aber kaum nahe. Java verhindert nicht, dass veränderliche Referenzen auf dasselbe Objekt in mehreren Objekten gespeichert werden. Dieser Artikel erklärt das besser: https://without.boats/blog/references-are-like-jumps/
Als kleines Quiz: Was gibt dieser Code aus? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Edit: Ich habe die doppelte Verneinung falsch gelesen. Auch beim erneuten Lesen finde ich es immer noch verwirrend. Soll das heißen, dass Java im Gegensatz zu JavaScript lokales Schlussfolgern hat?
Ich mag Graydons Texte normalerweise, aber dieser kann – wie viele Texte zu formalen Methoden – bei Leserinnen und Lesern, die das Feld nicht kennen, Missverständnisse hervorrufen. Es ist ein bisschen so, als würde man sagen, die Methode, Blei in Gold zu verwandeln, sei um eine Größenordnung verbessert worden, ohne dazuzusagen, dass bis zu praktischer Kosteneffizienz noch 29 Größenordnungen fehlen.
Macht keine Aliasing formale Verifikation deutlich einfacher? Ja. Heißt das, dass man reale Programme praktisch und kosteneffizient verifizieren kann? Ganz und gar nicht. Es gibt Programme, Schaltungen und Komponenten, die täglich formal verifiziert werden, aber sie sind eher die Ausnahme, relativ sehr klein und werden auf besonders sorgfältige Weise erstellt. Eigenschaften, die lokales Schlussfolgern unterstützen, sind wichtig, ändern aber praktisch nichts daran, wie sich die Korrektheit von Mainstream-Software auf solide Weise garantieren lässt.
Selbst Programme in einer Sprache, die weder Heap noch Pointer noch Integer hat, sondern nur boolesche Variablen, und in der Schleifen nicht mehr als zweimal durchlaufen werden können – also weit entfernt von Turing-Vollständigkeit –, lassen sich praktisch nicht verifizieren, weil sie auf TQBF reduziert werden können. Für manche Eigenschaften, etwa Speichersicherheit, ist das möglich, aber für das, was Software braucht, reicht es nicht. In den 1970er- bis 1990er-Jahren gab es die Hoffnung, dass lokale Garantien und die Struktur von Sprachen einen trotz unbeherrschbarer Worst-Case-Komplexität aus dem Worst Case heraushalten würden; später wurde gezeigt, dass das nicht so ist. Auch die Hoffnung, dass Programme, die Menschen tatsächlich schreiben, weit genug vom Worst Case entfernt sind, um gute Heuristiken zu ermöglichen, scheint inzwischen nicht mehr zu tragen.
Dazu gibt es einen Vortrag: https://pron.github.io/posts/correctness-and-complexity
Das zentrale Ergebnis ist, dass die meisten interessanten Eigenschaften, die man verifizieren möchte, nicht kompositionell sind. Selbst wenn man die Eigenschaft für jede Komponente P1...Pn einzeln beweist, wachsen die Kosten, diese Eigenschaft für P1 ○ ... ○ Pn zu beweisen, nicht nur superpolynomiell in n, sondern auch superpolynomiell in der Größe jeder Komponente. Mit anderen Worten: Es ist genauso schwer, als hätte man nichts zerlegt; Korrektheit lässt sich nicht zerlegen. Deshalb können „man kann ziemlich viel verifizieren“ und „das Verifizierbare ist nur ein Tropfen im Ozean“ gleichzeitig wahr sein, und in Diskussionen über formale Methoden fehlt diese Lücke häufig.
Du wiederholst seit über sechs Jahren auf HN hunderte Male dieselbe Argumentation, und trotz der vielen Kommentare, die du in dieser Zeit bekommen hast, ist kaum zusätzliche Nuance dazugekommen.
Es ist nicht völlig falsch, aber auch nicht völlig richtig. Viele Menschen, die sich für dieses Thema interessieren, hatten über hunderte Wiederholungen hinweg reichlich Gelegenheit, genau das zu zeigen; dass sich deine Position überhaupt nicht weiterentwickelt hat, ist erstaunlich. Diese Haltung klingt nach einer krankhaften Verschlossenheit und verschwendet die Zeit aller, die sich an der Diskussion beteiligen.
Ich denke, dass die Fokussierung auf Soundness dem Ziel korrekterer Software weniger hilft, als dass sie die Aufmerksamkeit von Methoden ablenkt, die in der Praxis tatsächlich bessere Ergebnisse erzielt haben. Es gibt praktische Methoden, die auch theoretisch gestützt sind und manchmal sogar Leute überraschen, die dachten, Soundness sei der einzige Weg: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Das passiert immer wieder. Während es bei sounden Methoden wichtige Verbesserungen gibt, erzielen unsounde Methoden in der Praxis deutlich größere Fortschritte hin zu korrekterer Software. Ein ganz aktuelles Beispiel ist https://antithesis.com. Natürlich können sounde Methoden in bestimmten Situationen leistungsfähiger und praktischer sein; das Thema ist also komplex.
Es ist vernünftig zu erwarten, dass man verifizieren können wird, ob kleine Rust-Libraries unsafe korrekt verwenden. Schon das allein wäre wirklich nützlich.
Ich habe gerade auch unter dem F*-Artikel einen entsprechenden Kommentar geschrieben. Rein von der Syntax her bevorzuge ich subjektiv F*/F# gegenüber Rust, aber für die Show-Control-Software, die ich entwickle, habe ich mich für Ada/SPARK2014 entschieden.
Wenn Rust Leute anziehen will, die sonst zu Ada/SPARK2014 greifen würden, braucht es einen offiziell veröffentlichten Standard wie bestehende Sprachen à la C, Common Lisp, Prolog, Fortran oder COBOL. AdaCore und Ferrous Systems arbeiten daran, formale Verifikationstools für Rust bereitzustellen, ähnlich wie bei Ada/SPARK2014, und damit kommt Rust ebenfalls in dieses Feld hinein; aber es gibt noch keinen veröffentlichten Standard, und das Erbe von Ada und SPARK2014 ist sehr groß.
Interessant ist, dass man Reference Counting als eine Art sofort ausgeführten, optimierten GC betrachten kann, der funktioniert, wenn man ihn strikt für azyklische Daten verwendet oder zyklische Lecks in Kauf nehmen kann. Python nutzt die im Artikel beschriebene Mischform aus Reference Counting und Tracing; ich habe auch produktive Deployments gesehen, die den Tracing-Collector nur einmal alle N Requests laufen lassen
Perl verwendet reines Reference Counting, hat aber Weak References. Damit kann man Daten aus Sicht des Reference Countings azyklisch machen, um den Preis, darauf achten zu müssen, an welcher Stelle einer zyklischen Struktur man Referenzen hält. Koka nutzt theoretisch Reference Counting, versucht aber in der Praxis, so viel wie möglich in die Compile-Zeit zu verlagern; wenn bei y = x + 1 garantiert ist, dass x nur eine Referenz hat und danach nicht mehr verwendet wird, kann für y derselbe Speicher wiederverwendet und eine In-Place-Änderung vorgenommen werden
Nim bietet ORC an, eine automatische Reference-Counting-Lösung plus Implementierung des Recycler-Algorithmus von Bacon+Rajan. Dieser Algorithmus ist darauf ausgelegt, in Reference-Counting-basierten Systemen nur Zyklen einzusammeln, und ist ziemlich schnell. Zurück zu Rust: Eine Stop-the-World-Implementierung des Recycler gibt es hier: https://github.com/fitzgen/bacon-rajan-cc und dieser Fork wird als Crate bacon-rajan-ccc veröffentlicht: https://github.com/mbartlett21/bacon-rajan-cc Im Abschnitt „Alternative“ der README sind weitere Experimente im selben Bereich verlinkt. Falls das Recycler-Paper schwer zu finden ist: Kopien habe ich unter https://trout.me.uk/gc/ gesammelt; wer einen ähnlichen Geschmack hat, dürfte auch die Paper unter https://trout.me.uk/lisp/ mögen
Auch Firefox verwendet Reference Counting zusammen mit einem zyklischen Collector auf Basis von Trial Deletion, um Zyklen zwischen C++-DOM-Objekten und JavaScript zu verwalten. Tatsächlich war Graydon für die frühe Implementierung verantwortlich
Bei der formalen Verifikation von Programmen werde ich ungeduldig. Der Beweis, dass ein Programm eine Spezifikation korrekt implementiert, ist theoretisch interessant, hat praktisch aber wenig Nutzen
Eine korrekte Spezifikation zu schreiben ist genauso schwierig wie korrektes Programmieren; das schwierige Problem wird also nicht gelöst, sondern nur verlagert. Es gibt praktische Einsatzgebiete für formale Methoden, aber man begegnet ihnen selten
Für eine vollständige Spezifikation stimmt das, aber das ist nicht das eigentliche Ziel. Meist will man einige zentrale Eigenschaften beweisen. Zum Beispiel, dass diese Funktion immer terminiert oder jene Funktion immer ein sortiertes Array zurückgibt
Sobald man so etwas kann, lässt es sich als Vorbedingung erzwingen. Etwa, dass man zeigen muss, dass ein Array bereits sortiert ist, bevor man es an eine bestimmte Funktion übergibt
Geschrieben am 15. Mai 2024, dem 9. Jahrestag von Rust 1.0
Ich habe den verlinkten Artikel von Boats gelesen; er war hervorragend. Es hat mich überrascht, dass Hoares Zitat von vor 50 Jahren immer noch relevant ist und so gut formuliert bleibt
Es wäre schön, wenn man auf einfachere Weise so etwas wie Typ-Guards zur Compile-Zeit verwenden könnte. Wenn Trait Bounds wuchern, werden Programme auf Type-Level schwer lesbar
Zum Beispiel Where <<::Output as G>::Output as H>::Output: HList + Z oder type Output = <<::Output as G>::Output as H>::Output;. Dann steckt man noch Cons>>> hinein und merkt, dass auch Zahlen wie TypeNums U8 intern selbst Verschachtelungen von Cons>> sind. In diesem Bereich kann man Fortschritte erzielen und die gewünschte Verifikation erreichen, aber die Fehlermeldungen können sich stark davon entfernen, wie menschliche Entwickler Code schreiben, und die Implementierung ist sehr schmerzhaft
Der Grund, warum die Developer Experience so erstaunlich ist: Das ist nicht „einfach eine Funktion“, sondern eine bestimmte Kombination aus Generics und assoziierten Typen. Ich möchte Prüfungen im Runtime-Stil verwenden, sie aber zur Compile-Zeit ausführen; dafür musste ich jedoch ziemlich anderen Code schreiben. Letztlich könnte es der Weg zu einer guten Erfahrung für Maintainer und Nutzer solcher formalen Analyseprojekte sein, Type-Level-Compile-Time-Rust einfacher, funktionaler und lesbarer zu machen. Kurz gesagt: Ich möchte comptime Rust. Außerdem frage ich mich, ob Future auf Basis von Pin<&mut Self> inzwischen schon fest zementiert ist. Ich würde gern mit anderen internen Implementierungen von async/await experimentieren, weiß aber nicht, wo ich anfangen soll
1 Kommentare
Hacker-News-Kommentare
Guter Artikel. Aus der Perspektive von jemandem, der früher Programmverifikation betrieben hat, wirkt Rust wie die nützlichste moderne Sprache für die Anwendung formaler Methoden.
Rusts Regeln beseitigen viele Fälle, die schwer zu formalisieren sind. Das verbleibende große Problem ist die Deadlock-Analyse aus Thread-Sicht und aus
Rc-/Borrowing-Sicht; die beiden sind bis zu einem gewissen Grad äquivalent. Wenn Rust eine statische Deadlock-Analyse hätte, würden wohl auch sichere dereferenzierbare Pointer möglich, und wenn man beweisen könnte, dass alle borrow-/upgrade-Aufrufe nicht fehlschlagen, ließe sich der Großteil des Reference Counting entfernen. Dann bekäme man, wo möglich, interne Veränderlichkeit praktisch kostenlos dazu.Das große Problem von Theorem Provers ist, dass sie von Leuten gebaut werden, die gern Theoreme beweisen; dadurch verlieren sie sich im Formalismus, und ihr Gespür für Programmierer und UI passt nicht zusammen. Die meisten Beweispflichten lassen sich mit SAT-Solvern erledigen, aber für schwierige Probleme braucht man schwergewichtigere Werkzeuge. Coq ist zu manuell, und der Autor hält ACL2 für zu funktional. Machine Learning kann bei der Richtungsweisung für Theorem Provers helfen. Den Beweis selbst ihm zu überlassen ist schwierig, aber aus Code, dessen Control Flow und Datennutzung weitgehend ähnlich sind, Beweispläne abzuleiten, scheint machbar.
Die Kryptoroutinen von Firefox und Wireguard wurden nicht in Rust geschrieben, sondern in F*, genauer gesagt in Low*, einem in F* eingebetteten Low-Level-DSL, und sind vollständig verifiziert.
https://project-everest.github.io/
https://mitls.org/
Das Problem bei der Anwendung solcher Tools auf die Verifikation externer Sprachen wie Rust ist, dass die Beweise nicht in der Zielsprache geschrieben werden und Entwickler daher zwei Sprachen lernen müssen. Aufgrund meiner Erfahrung mit Creusot, Arbeiten an Verus und Aeneas sowie Erfahrungen im Why3-Labor habe ich darüber nachgedacht, wie ein „verifikationsbewusstes Rust“ aussehen könnte. Wenn man eine solche Sprache von Anfang an entwirft, könnte ihre Verifizierbarkeit gegenüber Rust schrittweise deutlich besser werden, besonders an den schwierigen Stellen von Beweisen.
Was mir als eingebaute Funktion am meisten fehlt, ist etwas im Sinne von „lass quickcheck über meinen Beweis laufen“. Wenn man Code hat und versucht, eine Eigenschaft zu beweisen, die gar nicht wahr ist, kann man sich leicht die Haare raufen, weil man nicht versteht, warum der Beweis nicht klappt. Wenn man mitten im Beweis in einem unsinnigen Zustand landet, wäre es schön, wenn ein Befehl wie „erzeuge hier ein Gegenbeispiel“ ein Gegenbeispiel ausspucken würde. Beweise sind stark pfadabhängig und im Allgemeinen nicht einfach, aber diese Tools wirken sehr nah an Größe. Der Versuch, Code zu beweisen, muss auch die Möglichkeit widerspiegeln, dass dieser Code Bugs haben kann.
Der Prover leitet keinen falschen Beweis ab, sondern scheitert einfach daran, einen gültigen Beweis abzuleiten. Ich denke, es gibt nicht viele Machine-Learning-Anwendungen mit dieser Eigenschaft.
Tatsächlich sind Locks und Reference Counts in Rust Laufzeitstrukturen.
Arcbricht Rusts RAII-Modell erheblich, sodass scoped threads, deren Destruktor vor dem Ende des Scopes ausgeführt werden musste, entfernt werden mussten. Globale Reference Counts haben Probleme mit Zyklen und Leaks und werden wieder zu einem globalen Problem. Ganz wird man sie schwer los, aber ich glaube, es ist besser, sie in Arena-artige Scopes einzuschließen. Für Locks scheinen asymmetrische Datenstrukturen wie Channels nötig zu sein. In Go kann man Channels in Sender und Empfänger aufteilen und im sendenden goroutinedefer close(ch)setzen; selbst bei einer Panic ist garantiert, dass es ausgeführt wird, wenn der Rest des Threads endet. Es müssen nicht unbedingt Channels sein, aber wenn man Lese-/Schreib- bzw. Producer-/Consumer-Rollen trennt, wird das Schlussfolgern viel einfacher und dürfte auch der formalen Analyse helfen.Mir gefällt, dass es mit einem Zitat aus Hoares Paper von etwa 1973 begann und nun schon bis zu einem zweiten Artikel weitergeführt wurde. Ursprünglich hatte ich im HN-Thread zu boats Artikel einen langen Kommentar geschrieben und gesagt, dass es angesichts von boats Hintergrund zwar verständlich ist, dieses Zitat in eine Rust-zentrierte Perspektive zu kippen, dass dadurch aber der Umfang von Hoares Kritik künstlich verengt wird.
Nun hat Grayson dieses schmale Stück als Ausgangspunkt genommen, um einige interessante Bereiche und Designpunkte von Rust zu diskutieren. Ich halte meinen Kommentar weiterhin für richtig, aber die Diskussion, die sich aus Graysons Artikel ergeben hat, war ausreichend, um die technischen Einwände gegen den Ausgangsartikel aufzuwiegen.
Seitdem sind unsolide Verfahren entstanden, die über einfaches Testen hinausgehen, und meiner Ansicht nach sind unsolide Methoden den soliden inzwischen voraus.
Er hatte das Problem gefunden, und rückblickend wirkt die Lösung, shared XOR mutable per Typsystem zu erzwingen, wie ein kleiner Schritt. Hätte man damals erkannt, dass genau dieser kleine Schritt die Lösung ist, hätte das 50 Jahre enormen Schmerz erspart.
Aber das Zitat selbst scheint diese Sichtweise nicht zu stützen. Man kann es als Versuch sehen, Hoares allgemeinere Klage über die semantische Existenz von Referenzen an sich zu nehmen und auf Rusts Modell von nicht-aliasbehaftetem veränderlichem Zustand anzuwenden, um das Problem zu umgehen. Allerdings kommt das eher dem gleich, nur ein schmales Stück eines größeren Problems zu reparieren und dann zu sagen, das ganze Problem sei verschwunden. Die ausgelassenen Teile, insbesondere der Beginn des Abschnitts „Variables“ und das ALGOL-68-Beispiel, sprechen viel stärker dafür, dass Hoare nicht nur veränderlichen Zustand kritisierte, sondern das semantische Konzept von Referenzen an sich. Ich erkenne an, dass Rust versucht, einen Teil des Problems zu zähmen, aber ich sehe keine Sprache, die dieses Problem „behoben“ hätte.
Ich verstehe nicht ganz, warum dieser Artikel so viel Lob bekommt. Es wirkt, als würden mehrere Bereiche der Programmanalyse in einem einzigen Absatz abgehandelt. Ich mag Graydon und respektiere seine Perspektive, aber dieser Absatz ist übermäßig vereinfacht.
Die Erklärung, Sprachen mit GC hätten sich nicht die Mühe gemacht, starke Unterstützung für lokales Schlussfolgern bereitzustellen, ist ein Strohmann. Es gab Sprachen wie Pony, die Regionen im Typsystem haben und trotzdem GC verwenden. Außerdem gibt es ganze Gebiete der Pointer-Analyse und Escape-Analyse, die Eindeutigkeit inferieren und bestimmen, ob zwei Referenzen Aliasse sein können. Auch der Kern statischer Typisierung besteht darin, den Heap mithilfe der Techniken Klassen und Felder in nicht miteinander aliasbehaftete Teile aufzuteilen. Es geht hier nicht um JavaScript, und man sollte nicht so tun, als gäbe es in Java/C#/Scala und zahllosen GC-Sprachen kein lokales Schlussfolgern über veränderlichen Zustand.
Klassen und Felder bieten kein vollständiges lokales Schlussfolgern über veränderlichen Zustand. Denn Klasse/Objekt A kann vom veränderlichen Zustand von Klasse/Objekt B abhängig werden. Java-artige Klassenvererbung fügt von sich aus zusätzliche Komplexität hinzu, während ein Programm im Laufe der Zeit evolviert.
Gegenbeispiele gibt es natürlich, aber wenn man sich Mainstream-GC-Allzwecksprachen wie Java, C# und Python ansieht, stimmt die Aussage. Man kann die ursprüngliche Idee der Objektorientierung so interpretieren, dass sie dem heutigen Actor Model näherstand und dass man besessene Datenstrukturen nur per Message Passing verändern wollte. Die tatsächlichen Implementierungen von Objektorientierung kommen diesem Ziel aber kaum nahe. Java verhindert nicht, dass veränderliche Referenzen auf dasselbe Objekt in mehreren Objekten gespeichert werden. Dieser Artikel erklärt das besser: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Edit: Ich habe die doppelte Verneinung falsch gelesen. Auch beim erneuten Lesen finde ich es immer noch verwirrend. Soll das heißen, dass Java im Gegensatz zu JavaScript lokales Schlussfolgern hat?
Ich mag Graydons Texte normalerweise, aber dieser kann – wie viele Texte zu formalen Methoden – bei Leserinnen und Lesern, die das Feld nicht kennen, Missverständnisse hervorrufen. Es ist ein bisschen so, als würde man sagen, die Methode, Blei in Gold zu verwandeln, sei um eine Größenordnung verbessert worden, ohne dazuzusagen, dass bis zu praktischer Kosteneffizienz noch 29 Größenordnungen fehlen.
Macht keine Aliasing formale Verifikation deutlich einfacher? Ja. Heißt das, dass man reale Programme praktisch und kosteneffizient verifizieren kann? Ganz und gar nicht. Es gibt Programme, Schaltungen und Komponenten, die täglich formal verifiziert werden, aber sie sind eher die Ausnahme, relativ sehr klein und werden auf besonders sorgfältige Weise erstellt. Eigenschaften, die lokales Schlussfolgern unterstützen, sind wichtig, ändern aber praktisch nichts daran, wie sich die Korrektheit von Mainstream-Software auf solide Weise garantieren lässt.
Selbst Programme in einer Sprache, die weder Heap noch Pointer noch Integer hat, sondern nur boolesche Variablen, und in der Schleifen nicht mehr als zweimal durchlaufen werden können – also weit entfernt von Turing-Vollständigkeit –, lassen sich praktisch nicht verifizieren, weil sie auf TQBF reduziert werden können. Für manche Eigenschaften, etwa Speichersicherheit, ist das möglich, aber für das, was Software braucht, reicht es nicht. In den 1970er- bis 1990er-Jahren gab es die Hoffnung, dass lokale Garantien und die Struktur von Sprachen einen trotz unbeherrschbarer Worst-Case-Komplexität aus dem Worst Case heraushalten würden; später wurde gezeigt, dass das nicht so ist. Auch die Hoffnung, dass Programme, die Menschen tatsächlich schreiben, weit genug vom Worst Case entfernt sind, um gute Heuristiken zu ermöglichen, scheint inzwischen nicht mehr zu tragen.
Dazu gibt es einen Vortrag: https://pron.github.io/posts/correctness-and-complexity
Das zentrale Ergebnis ist, dass die meisten interessanten Eigenschaften, die man verifizieren möchte, nicht kompositionell sind. Selbst wenn man die Eigenschaft für jede Komponente P1...Pn einzeln beweist, wachsen die Kosten, diese Eigenschaft für P1 ○ ... ○ Pn zu beweisen, nicht nur superpolynomiell in n, sondern auch superpolynomiell in der Größe jeder Komponente. Mit anderen Worten: Es ist genauso schwer, als hätte man nichts zerlegt; Korrektheit lässt sich nicht zerlegen. Deshalb können „man kann ziemlich viel verifizieren“ und „das Verifizierbare ist nur ein Tropfen im Ozean“ gleichzeitig wahr sein, und in Diskussionen über formale Methoden fehlt diese Lücke häufig.
Es ist nicht völlig falsch, aber auch nicht völlig richtig. Viele Menschen, die sich für dieses Thema interessieren, hatten über hunderte Wiederholungen hinweg reichlich Gelegenheit, genau das zu zeigen; dass sich deine Position überhaupt nicht weiterentwickelt hat, ist erstaunlich. Diese Haltung klingt nach einer krankhaften Verschlossenheit und verschwendet die Zeit aller, die sich an der Diskussion beteiligen.
Das passiert immer wieder. Während es bei sounden Methoden wichtige Verbesserungen gibt, erzielen unsounde Methoden in der Praxis deutlich größere Fortschritte hin zu korrekterer Software. Ein ganz aktuelles Beispiel ist https://antithesis.com. Natürlich können sounde Methoden in bestimmten Situationen leistungsfähiger und praktischer sein; das Thema ist also komplex.
unsafekorrekt verwenden. Schon das allein wäre wirklich nützlich.Ich habe gerade auch unter dem F*-Artikel einen entsprechenden Kommentar geschrieben. Rein von der Syntax her bevorzuge ich subjektiv F*/F# gegenüber Rust, aber für die Show-Control-Software, die ich entwickle, habe ich mich für Ada/SPARK2014 entschieden.
Wenn Rust Leute anziehen will, die sonst zu Ada/SPARK2014 greifen würden, braucht es einen offiziell veröffentlichten Standard wie bestehende Sprachen à la C, Common Lisp, Prolog, Fortran oder COBOL. AdaCore und Ferrous Systems arbeiten daran, formale Verifikationstools für Rust bereitzustellen, ähnlich wie bei Ada/SPARK2014, und damit kommt Rust ebenfalls in dieses Feld hinein; aber es gibt noch keinen veröffentlichten Standard, und das Erbe von Ada und SPARK2014 ist sehr groß.
Interessant ist, dass man Reference Counting als eine Art sofort ausgeführten, optimierten GC betrachten kann, der funktioniert, wenn man ihn strikt für azyklische Daten verwendet oder zyklische Lecks in Kauf nehmen kann. Python nutzt die im Artikel beschriebene Mischform aus Reference Counting und Tracing; ich habe auch produktive Deployments gesehen, die den Tracing-Collector nur einmal alle N Requests laufen lassen
Perl verwendet reines Reference Counting, hat aber Weak References. Damit kann man Daten aus Sicht des Reference Countings azyklisch machen, um den Preis, darauf achten zu müssen, an welcher Stelle einer zyklischen Struktur man Referenzen hält. Koka nutzt theoretisch Reference Counting, versucht aber in der Praxis, so viel wie möglich in die Compile-Zeit zu verlagern; wenn bei
y = x + 1garantiert ist, dassxnur eine Referenz hat und danach nicht mehr verwendet wird, kann füryderselbe Speicher wiederverwendet und eine In-Place-Änderung vorgenommen werdenNim bietet ORC an, eine automatische Reference-Counting-Lösung plus Implementierung des Recycler-Algorithmus von Bacon+Rajan. Dieser Algorithmus ist darauf ausgelegt, in Reference-Counting-basierten Systemen nur Zyklen einzusammeln, und ist ziemlich schnell. Zurück zu Rust: Eine Stop-the-World-Implementierung des Recycler gibt es hier: https://github.com/fitzgen/bacon-rajan-cc und dieser Fork wird als Crate bacon-rajan-ccc veröffentlicht: https://github.com/mbartlett21/bacon-rajan-cc Im Abschnitt „Alternative“ der README sind weitere Experimente im selben Bereich verlinkt. Falls das Recycler-Paper schwer zu finden ist: Kopien habe ich unter https://trout.me.uk/gc/ gesammelt; wer einen ähnlichen Geschmack hat, dürfte auch die Paper unter https://trout.me.uk/lisp/ mögen
Bei der formalen Verifikation von Programmen werde ich ungeduldig. Der Beweis, dass ein Programm eine Spezifikation korrekt implementiert, ist theoretisch interessant, hat praktisch aber wenig Nutzen
Eine korrekte Spezifikation zu schreiben ist genauso schwierig wie korrektes Programmieren; das schwierige Problem wird also nicht gelöst, sondern nur verlagert. Es gibt praktische Einsatzgebiete für formale Methoden, aber man begegnet ihnen selten
Sobald man so etwas kann, lässt es sich als Vorbedingung erzwingen. Etwa, dass man zeigen muss, dass ein Array bereits sortiert ist, bevor man es an eine bestimmte Funktion übergibt
Geschrieben am 15. Mai 2024, dem 9. Jahrestag von Rust 1.0
Ich habe den verlinkten Artikel von Boats gelesen; er war hervorragend. Es hat mich überrascht, dass Hoares Zitat von vor 50 Jahren immer noch relevant ist und so gut formuliert bleibt
Es wäre schön, wenn man auf einfachere Weise so etwas wie Typ-Guards zur Compile-Zeit verwenden könnte. Wenn Trait Bounds wuchern, werden Programme auf Type-Level schwer lesbar
Zum Beispiel
Where <<::Output as G>::Output as H>::Output: HList + Zodertype Output = <<::Output as G>::Output as H>::Output;. Dann steckt man nochCons>>>hinein und merkt, dass auch Zahlen wie TypeNumsU8intern selbst Verschachtelungen vonCons>>sind. In diesem Bereich kann man Fortschritte erzielen und die gewünschte Verifikation erreichen, aber die Fehlermeldungen können sich stark davon entfernen, wie menschliche Entwickler Code schreiben, und die Implementierung ist sehr schmerzhaftDer Grund, warum die Developer Experience so erstaunlich ist: Das ist nicht „einfach eine Funktion“, sondern eine bestimmte Kombination aus Generics und assoziierten Typen. Ich möchte Prüfungen im Runtime-Stil verwenden, sie aber zur Compile-Zeit ausführen; dafür musste ich jedoch ziemlich anderen Code schreiben. Letztlich könnte es der Weg zu einer guten Erfahrung für Maintainer und Nutzer solcher formalen Analyseprojekte sein, Type-Level-Compile-Time-Rust einfacher, funktionaler und lesbarer zu machen. Kurz gesagt: Ich möchte
comptimeRust. Außerdem frage ich mich, obFutureauf Basis vonPin<&mut Self>inzwischen schon fest zementiert ist. Ich würde gern mit anderen internen Implementierungen vonasync/awaitexperimentieren, weiß aber nicht, wo ich anfangen soll