C*: Programmieren und Verifizieren in einer Sprache vereint
C*: Unifying Programming and Verification in C
C* ist ein neuer Sprachansatz, der C um eingebaute Verifikationsfähigkeiten erweitert. Entwickelt von einem Team um Yiyuan Cao und Qinxiang Cao, zielt C* darauf ab, die Kluft zwischen Programmierung und formaler Verifikation zu überbrücken. Es integriert einen symbolischen Ausführungskern und einen LCF-basierten Proof-Kernel direkt in C, sodass Entwickler Beweis-Codeblöcke neben dem Implementierungscode platzieren und den Beweisstatus in Echtzeit aktualisieren können. Die ausdrucksstarke und erweiterbare Beweisunterstützung ermöglicht wiederverwendbare Bibliotheken für logische Definitionen, Theoreme und programmierbare Beweisautomatisierung. In einer Evaluation mit kleinen C-Programmen und der attach-Funktion des pKVM-Buddy-Allokators zeigte der Prototyp, dass er einen breiten Teilbereich von C-Idiomen verifizieren und komplexe Reasoning-Aufgaben in realen Szenarien bewältigen kann.
C* vereint die Entwicklung von Implementierungs- und Beweis-Code, indem es C als gemeinsame Sprache verwendet.
- eggy
Ich bin schon eine Weile auf diesem Trip. Ich habe mich für Ada/SPARK entschieden. Ada 2022 wird ein neues SPARK-2014-Update speisen. Ja, sie sind beide wortreich, wenn man so etwas nicht mag und keine Pascal-ähnliche Syntax mag. Glaub mir, ich mag APL/J/k/uiua/BQN und Forth und ASM. Normalerweise bin ich Syntax-agnostisch, solange die Programmiersprache und das Ökosystem (wichtiger als die meisten denken) deine Bedürfnisse erfüllen. Ich habe Rust 2018 ausprobiert und dann nochmal 2023, fand es aber sehr komplex und, na ja, kein Fan der Syntax. Ich hätte eher eine ML- oder Haskell-ähnliche Syntax bevorzugt. Zig schien nett, aber ein anderer Anwendungsfall und zu neu. Schließlich sind Ada/SPARK seit Jahrzehnten in riesigen, hochzuverlässigen, hochsicheren Anwendungen im Einsatz. Rust bekommt etwas von ihrer Liebe ab und umgekehrt. AdaCore hatte einen verifizierten Rust-Compiler erstellt, aber mit einem realen Produkt (Blacktail-Hoist) in Arbeit brauchen wir ein Toolset und Garantien sowie einfache Prüfung und Akzeptanz, um hohe Sicherheits- und Standardzertifizierungen zu erreichen. Denk an Luft- und Raumfahrt, Verteidigung, Bahn und Automobil. Ich habe 1977 mit dem Programmieren angefangen, daher gibt es immer einen Platz in meinem Herzen für ASM/C. Ich habe mit F#, F* und LOW von Microsoft gespielt, und sie sind gut, aber sie und Rust haben einfach nicht das reale Erbe von Ada/SPARK. Ich habe Shen verwendet, um einige formal verifizierte Modelle von weniger sicherheitskritischen Bereichen unserer Software zu schreiben, und ich finde es erfrischend, aber mein Tagesjob ist es, mich auf Ada/SPARK zu konzentrieren, bis Rust mit einem formal verifizierten, bewährten t […]
- IsTom
Ich mag das Konzept der Separation Logic wie jeder andere, aber ich glaube nicht, dass das hier es ist. Schau dir nur die Beispiele an, wo allein die Schleifeninvarianten länger sind als das gesamte Beispiel. Es ist nicht nur ein Problem der Ergonomie, sondern es lässt auch viel Raum für Spezifikationsfehler. Und ich vermute, dass die Schnittmenge von Leuten, die C-Code schreiben, den man mit formalen Verifikationsleuten verifizieren möchte, nicht besonders groß ist.
- gavinray
Ich denke wirklich, dass verifikationsbewusste Sprachen zur Notwendigkeit werden. Ich habe kürzlich etwas darüber geschrieben. https://gavinray97.github.io/blog/design-by-contract-and-eff...
- slowcache
Ich finde formale Verifikation ein super interessantes Feld, aber das ist für mich ein No-Go, weil ich kein umgedrehtes E auf meiner Tastatur habe.
- Taikonerd
Die Autoren zitieren das, aber nur um es zu erwähnen: Das klingt nach F*, einer weiteren beweisorientierten Sprache. (https://fstar-lang.org/) F* gehört zur ML-Familie von Sprachen, sieht also ganz anders aus als C*.