QAL.
eine Runde · alle Prüfungen · 0,28 s

Ein Agent schreibt Code und weiß in derselben Runde, ob er stimmt.

In QAL liegt Code nicht in Dateien, sondern als geprüfte Funktionsknoten in einem Speicher. Jeder Schreibvorgang wird sofort getypt, bewiesen, getestet und mit dem ganzen Programm neu verknüpft. Die Antwort kommt in unter einer halben Sekunde, als JSON.

Query&AgentLanguage
Agent → qal_defineQAL
type Acct = { id: Int, balance: Int }

fn deposit(a: Acct, n: Int) -> Acct
  req n >= 1
  ens r.balance > a.balance
= Acct { id: a.id, balance: a.balance + n }

test deposit_adds =
  deposit(Acct { id: 1, balance: 5 }, 3).balance == 8
Speicher → Agent, dieselbe RundeJSON
{
  "defined": ["Acct", "deposit", "deposit_adds": "added"],
  "proofs":  ["req n >= 1" at the call in deposit_adds: "proven",
             "ens r.balance > a.balance": "unknown", still checked at run time],
  "tests":   ["deposit_adds": passed],
  "warnings": [{ "code": "E0804", "kind": "property_traps",
    "message": "`deposit` trapped in 3 of 103 generated runs:
      Int overflow in `+` (64-bit) {left: 1, right: 9223372036854775807}",
    "hints": ["... say so with a `req` on `deposit` that bounds them"] }]
}

Echte Antwort von qal_define auf genau diesen Code, gekürzt, in 0,44 s. Kein Test prüfte den Überlauf bei einem Kontostand nahe dem Int-Maximum; die Property-Tests haben ihn in derselben Runde gefunden.

0,28 sein define mit allen Prüfungen, 66 Funktionen
0,43 sderselbe Ablauf bei 1520 Definitionen
95 / 96Stufen mit allen verborgenen Tests grün
11 / 13eingebaute Fehler, die E0807 ohne Tests meldet
Der Name

QAL steht für Query & Agent Language

Beide Hälften des Namens beschreiben, wie die Sprache arbeitet.

Q
Query

Code wird abgefragt, nicht durchsucht

Der Code liegt in einem Speicher statt in Dateien. Ein Agent fragt ihn ab: wer eine Funktion verwendet (qal_query), wie eine Definition aussieht (qal_view), wie sie sich verändert hat (qal_history). Jede Antwort ist strukturiertes JSON statt Text, den man erst auswerten muss.

A
Agent

Gebaut für den, der schreibt

Die Sprache ist für KI-Agenten entworfen, nicht für Menschen am Editor. Deshalb prüft jeder Schreibvorgang sofort alles, jeder Fehler hat einen Code, einen Pfad und einen Hinweis zur Behebung, und jede Wirkung nach außen muss ausdrücklich freigegeben werden.

Warum jetzt

Der nächste Schritt: Sprachen für die Zeit, in der Agenten schreiben

Alle verbreiteten Programmiersprachen wurden für Menschen am Editor entworfen. Inzwischen schreiben KI-Agenten einen wachsenden Teil des Codes. QAL setzt dort an, wo sich dadurch der Engpass verschoben hat.

Was sich geändert hat

Code zu erzeugen ist billig geworden

Ein Agent schreibt in Sekunden, wofür ein Mensch Stunden braucht. Die Menge an Code wächst schneller, als Menschen ihn lesen und prüfen können.

Wo der Engpass jetzt liegt

Teuer ist das Prüfen

Ob der Code stimmt, zeigt sich in heutigen Sprachen erst später: im Testlauf, im Review, im Betrieb. Ein Agent erfährt es oft gar nicht oder zu spät.

Was QAL daraus macht

Prüfen ist Teil des Schreibens

Jeder Schreibvorgang wird sofort getypt, bewiesen, getestet und mit dem Programm verknüpft. Vertrauen entsteht aus maschinell geprüften Garantien, nicht aus Hoffnung.

Worum es gehtSprachen für MenschenQAL, eine Sprache für Agenten
Wo Code liegtTextdateien, die man durchsuchtgeprüfte Knoten im Speicher, die man abfragt
FehlermeldungenText für MenschenJSON mit Code, Pfad und Hinweis zur Behebung
Testsein späterer, eigener Schrittlaufen bei jedem Schreiben mit, so weit die Änderung reicht
VerträgeKommentare oder Laufzeit-Assertsvom Z3-Beweiser beim Schreiben bewiesen
Nebenwirkungenunsichtbar im Codeim Typ deklariert und einzeln freigegeben
Unbemerkte Rückschrittefindet ein Mensch, wenn er Glück hatmeldet das Verhaltensgedächtnis in derselben Runde
KI-Aufrufe im Programmein ungeprüfter API-Aufrufein Effekt mit Budget, Aufzeichnung und deterministischen Tests
Mehrere AgentenKonflikte im VersionsverlaufRollen, Leases, Merge-Tor und signierte Geschichte

Unsere These: Je mehr Code Agenten schreiben, desto weniger kann Vertrauen davon kommen, dass ein Mensch jede Zeile liest. Es muss aus der Sprache selbst kommen. QAL ist um diesen Gedanken herum gebaut. Was davon heute gemessen ist und was noch nicht besser ist, steht weiter unten bei den Zahlen und den Grenzen.

Die eine Runde

Fünf Prüfungen, ein Aufruf

Andere Sprachen verteilen diese Schritte auf Compiler, Testlauf, Linter und Review. In QAL sind sie die Antwort auf jedes Schreiben. Der Agent muss nichts davon selbst anstoßen; ein separates qal_test oder qal_prove danach ist nicht nötig.

Typen und Effekte

Passt es?

Typprüfung, Vollständigkeit jedes match, und jede Funktion nennt, was sie darf: !io, !fs, !net, !db, !model.

Z3-Beweis

Gilt der Vertrag?

Jedes ens und das req jeder Funktion an jedem Aufruf. Ein widerlegter Vertrag wird nicht gespeichert, die Diagnose enthält ein Gegenbeispiel.

Tests

Bricht etwas?

Alle gespeicherten Tests, die die Änderung erreichen, auch über andere Funktionen hinweg.

Property-Tests

Und an den Rändern?

Jede definierte reine Funktion bei 0, ±1, leeren Werten und an den Grenzen ihres req; dazu die Typ-Invarianten.

Neu verknüpfen

Stimmt der Rest?

Alle abhängigen Definitionen bekommen neue Hashes und werden mitgeprüft.

+ E0807

Das Verhaltensgedächtnis: Frühere echte Programmläufe werden wiederholt. Ändert ein define ihre Ausgabe, meldet die Antwort genau diese Läufe, einmal, mit alter und neuer Ausgabe.

Selbst ausprobieren

Der echte Compiler, hier in deinem Browser

Der QAL-Compiler ist in QAL geschrieben und zu WebAssembly übersetzt. Genau dieses Modul, 444 KB, läuft jetzt auf deinem Rechner. Schreib Code oder nimm ein Beispiel: Die Antwort ist dieselbe, die ein Agent bekommt.

Compiler wird geladen …
Noch nicht geprüft

Sobald der Compiler geladen ist, wird geprüft, während du tippst.

Im Browser laufen Parser, Typprüfung, Effektprüfung und Vollständigkeit der match-Ausdrücke. Die Z3-Beweise, die Tests und der Speicher laufen im vollständigen Werkzeug qal.

Alles, was QAL kann

Der vollständige Atlas

Jede Fähigkeit der Sprache, des Speichers und der Werkzeuge, mit dem, was sie für einen Agenten bedeutet. Zusammengestellt aus der Sprachreferenz und der Hilfe von qal, Stand 26. Oktober 2026.

01 · Sprache

Klein, streng, ohne Überraschungen

Alles ist ein Ausdruck. Es gibt kein null, keine Ausnahmen, keine impliziten Umwandlungen und keine Schleifen.

TypenInt (64 Bit), Float, Bool, Unit, Str, Bytes, List[T], Map[K, V] (nach Schlüssel geordnet), Option[T], Result[T, E] und Funktionstypen.
Records und VariantenEigene Typen als Record oder als Aufzählung mit Daten.type Shape = Circle(Int) | Rect(Int, Int) | Dot
GenericsGenerische Typen und Funktionen; die Typargumente werden beim Aufruf abgeleitet.fn swap[A, B](p: Pair[A, B]) -> Pair[B, A]
Vollständiges Pattern MatchingMuster mit Konstanten, Varianten, Records und Wächtern. Jedes match muss alle Fälle abdecken.
ClosuresAnonyme Funktionen, die ihre Umgebung einfangen. Werte sind unveränderlich; Funktionen sind Werte.map(xs, fn(x) => x * k)
Effekte im TypWer liest, schreibt oder ins Netz geht, sagt es: !io !fs !time !rand !net !db !model. Aufrufer erben die Vereinigung.
Effekt-PolymorphieEine Funktion nimmt die Effekte ihres Callbacks an; mit einem reinen Callback bleibt sie rein.fn each[T, !e](xs: List[T], f: fn(T) -> Unit !e) -> Unit !e
Rekursion statt SchleifenEin Aufruf in Endposition ist eine Schleife. Listen werden mit map, filter, fold und range verarbeitet.
Exakte Ganzzahlena * b / c rechnet mit 128-Bit-Zwischenergebnis exakt. Ein echter Überlauf und Division durch null brechen ab, statt falsch weiterzurechnen.
Platzhaltertodo() steht für einen noch fehlenden Rumpf beliebigen Typs; ausgeführt bricht er mit E0540 ab.
02 · Verifikation

Beweisen, testen, erinnern

Vier Netze, die bei jedem Schreiben laufen: Beweise, Tests, Property-Tests und das Verhaltensgedächtnis.

Verträgereq ist die Vorbedingung, ens die Nachbedingung, r das Ergebnis. Zur Laufzeit gelten sie immer.fn sqrt_floor(n: Int) -> Int req n >= 0 ens r * r <= n
Z3-BeweiseExakt für Int und Bool, mit den Verträgen der aufgerufenen Funktionen. Widerlegt: nicht gespeichert, mit Gegenbeispiel. Nicht beweisbar: unknown mit Grund, zur Laufzeit geprüft.
Betroffene TestsEin define führt jeden gespeicherten Test aus, der eine geänderte Funktion erreicht, auch über Umwege.
Randwert-Property-TestsJede definierte reine Funktion an 0, ±1, leeren Werten und den Grenzen ihres req. Eingaben werden gezielt so gebaut, dass sie die Vorbedingung erfüllen.
Generierte Property-Testsqal_test prüft jede reine Funktion mit ens an 100 Eingaben; ein Fehler kommt mit verkleinertem Gegenbeispiel.
Typ-InvariantenEine reine Funktion inv_T ist die Regel für Typ T. Jede Funktion, die ein T nimmt oder liefert, wird darauf geprüft, auch tief in Listen und Records.
Verhaltensgedächtnis (E0807)Frühere Programmläufe werden bei jedem define wiederholt, bis zu 64 in 2 s. Geänderte Ausgaben werden einmal gemeldet und sind danach die neue Grundlage.
Warnung bei ungetesteter ÄnderungErsetzt ein define eine Funktion ohne einen Test, warnt E0806: jede neue Regel soll im selben Schritt einen Test bekommen.
Gedächtnis für KorrekturenWurde ein Fehler früher schon behoben, nennt die neue Diagnose die damalige Lösung; qal_recall listet frühere Korrekturen.
Beweise nach HashErgebnisse werden pro Definition und Hash gespeichert. Was sich nicht geändert hat, wird nicht noch einmal bewiesen.
03 · Speicher

Code als adressierte Knoten

Ein SQLite-Speicher in .qal/store.db. Jede Definition steht dort unter dem SHA-256 ihrer kanonischen Form.

Nur Geprüftes wird gespeichertWas nicht parst oder nicht typt, kommt gar nicht in den Speicher. Jeder Fehler ist eine JSON-Diagnose mit Pfad und Hinweisen.
Ersetzen mit NeuverknüpfungEin bestehender Name wird ersetzt. Bei gleicher Signatur werden alle Verwender automatisch neu verknüpft und geprüft.
SignaturänderungenAbhängige, die weiter passen, ziehen mit; die anderen werden mit ihren Fehlern abgelehnt, außer derselbe Aufruf definiert sie neu.
Umbenennen ohne Neuschreibenqal_rename ändert keinen Hash; alle Verwender folgen dem neuen Namen.
Sicheres Löschenqal_delete entfernt nur, was niemand mehr verwendet.
AbfragenNach Name, Typ-Muster oder Verwendern; eine Übersicht mit Verträgen, Verwendern und Tests (--outline).
VerlaufJede Änderung jedes Namens mit altem und neuem Hash, Zeitpunkt und Agent.
Inkrementelles PrüfenGeprüft und gehasht wird nur, was sich ändert, und das Ergebnis ist byte-gleich mit der vollständigen Prüfung. Bei 1520 Definitionen sind es 0,43 statt 1,7 s.
PaketeTeile des Speichers lassen sich als .qalpkg exportieren, importieren und installieren, aus einer Datei oder von einer URL.
Mehrere SchreiberGleichzeitige Schreibvorgänge werden über eine Sperre hintereinander gereiht; ein Beweis läuft dabei außerhalb der Sperre.
04 · Ausführung

WebAssembly mit festen Grenzen

Jedes Programm wird zu WebAssembly übersetzt und läuft in Wasmtime, abgeschottet vom System.

SandboxGrenzen für Rechenzeit, Speicher (256 MiB für Programme), Ausgabe und Laufzeit. Ein Effekt ohne Freigabe ist im Programm gar nicht verfügbar.
Fein dosierte Freigabenfs:<dir> nur für ein Verzeichnis, net:<host>[:port] nur für einen Rechner, db:mem für eine frische Datenbank im Speicher.qal run main --allow io,fs:data,net:api.example.org
Programme ausführenqal_run startet main(args) mit Argumenten und Eingabe; der Rückgabewert ist der Exit-Code.
Funktionen direkt aufrufenqal_call ruft jede Funktion mit JSON-Argumenten auf, ohne ein main zu schreiben.
Viele Fälle in einem Aufrufcases führt mehrere Eingaben nacheinander aus, in qal_run und direkt nach einem define.
Ein eigenständiges Modul bauenqal build erzeugt das WebAssembly-Modul einer Funktion.
05 · Dienste

HTTP, Datenbank, Netz

QAL-Programme können Webdienste sein, SQLite benutzen und andere Dienste aufrufen, mit eingebauten Typen dafür.

HTTP-HandlerEin Dienst ist eine Funktion von Anfrage zu Antwort; beliebige Effekte sind erlaubt.fn handle(rq: HttpRequest) -> HttpResponse
HTTP-Serverqal serve mit Arbeitern, Warteschlange, Zeitlimits, Größengrenzen für Anfrage und Antwort sowie Rechen- und Speichergrenzen pro Anfrage.
Anfragen testenqal_request spielt Anfragen gegen einen Handler ab, ohne Server und ohne Netz.
SQLite mit geprüftem SQLdb_exec und db_query nehmen nur ein SQL-Literal mit ?-Platzhaltern, eine Anweisung, keine PRAGMA- oder Transaktionsbefehle. Das wird schon beim Prüfen kontrolliert.
TransaktionenEine Transaktion pro Ausführung; festgeschrieben wird nur bei Erfolg, etwa Status 200 bis 399 oder Exit-Code 0.
Ausgehende Aufrufehttp(call) mit typisierten Fehlern (verweigert, ungültig, Verbindung, Zeitüberschreitung, zu groß). Weiterleitungen werden nicht verfolgt.
06 · KI-Aufrufe

Modelle als budgetierter Effekt

Programme können selbst ein Sprachmodell fragen. Das ist ein Effekt wie jeder andere: deklariert, freigegeben und begrenzt.

std.modelask liefert Text, ask_full zusätzlich Modell, Tokens und Kosten, ask_json geparstes JSON nach einem Schema.
BudgetJeder Aufruf wird gegen ein festes Budget in Euro gebucht, aufgerundet. Ist es aufgebraucht, kommt ModelBudgetExceeded statt eines weiteren Aufrufs.
AufzeichnungJede Antwort wird nach Prompt, Schema und Modell gespeichert. Dieselbe Frage kostet beim zweiten Mal nichts.
Deterministisches Abspielen--replay spielt nur Aufgezeichnetes ab, ohne Netz und ohne Schlüssel. Tests dürfen ein Modell fragen und sehen immer nur aufgezeichnete Antworten.
07 · Standardbibliothek

231 Definitionen in 7 Modulen

Automatisch in jedem Projekt vorhanden und schreibgeschützt. Jeder Name ist vollständig, etwa std.json.parse.

std.jsonJSON lesen, schreiben und durchsuchen; mit 77 Definitionen das größte Modul.
std.routeRouten für HTTP-Dienste, generisch über den Ergebnistyp (38 Definitionen).
std.strWeitere Funktionen für Zeichenketten über die eingebauten hinaus (35).
std.http und std.urlHilfen für Anfragen, Antworten und Kopfzeilen (28) sowie zum Zerlegen und Kodieren von URLs (27).
std.dbBequemer Zugriff auf Zeilen und Spalten von Datenbankergebnissen (22).
std.modelDie Modellaufrufe aus Abschnitt 06 (4).
Eingebaute FunktionenFür Zeichenketten, Listen, Maps, Bytes, Zahlen und das System: split, fold, map_put, sort_str, compare, read_line, now_ms, rand_int und weitere.
08 · Werkzeuge

Für Agenten und für Menschen

Agenten sprechen über einen MCP-Server mit dem Speicher, Menschen über die Kommandozeile. Beide nutzen dieselben Operationen.

MCP-Server mit 20 Werkzeugenqal_define, qal_test, qal_prove, qal_run, qal_call, qal_view, qal_query, qal_history, qal_rename, qal_delete, qal_build, qal_request, qal_recall und die Team-Werkzeuge.
Kommandozeileinit, define, view, query, history, rename, delete, test, prove, run, call, build, serve, request, export, import, install, recall, team, verify.
Dateien prüfen und formatierenqal check und qal fmt arbeiten auch auf QAL-Dateien außerhalb eines Speichers.
Editor-Anbindungqal lsp ist ein Language Server für Editoren.
Kompakte ReferenzDie Sprachreferenz liegt der Beschreibung von qal_define bei: höchstens 68 Zeilen, damit ein Agent sie bei jedem Start mitlesen kann.
Korrekturen übernehmenqal corrections import übernimmt gesammelte Korrekturen in das Gedächtnis eines Projekts.
09 · Team

Mehrere Agenten, klare Rollen

Ein Team-Speicher lässt mehrere Agenten zusammenarbeiten, mit Rollen, Änderungssätzen und einer lückenlos signierten Geschichte.

Vier RollenArchitektur legt Schnittstellen und Verträge fest, Implementierung füllt Rümpfe, Verifikation schreibt Tests und prüft, Review liest und gibt frei.
ÄnderungssätzeCode entsteht nur in eigenen Änderungssätzen; der Hauptstand ändert sich nur durch einen Merge.
LeasesWer einen Namen schreibt, hält ihn. Ein anderer Änderungssatz bekommt E0901 mit dem Namen des Halters.
Merge-TorEin Merge braucht „verified“ und „approve“ von anderen als dem Eigentümer. Er spielt die Änderungen neu ein, beweist neu und führt jeden Test aus.
Rebase mit KonfliktmarkenBei Konflikten wird der Hauptstand neue Basis; widersprüchliche Namen behalten die eigene Fassung mit einer Marke, bis sie neu definiert sind.
Signierte GeschichteJeder Schreibvorgang ist ein Ed25519-signierter Eintrag; qal verify prüft die ganze Kette. Sitzungen sind an Mitglieder gebunden.
10 · Compiler

In sich selbst geschrieben

Der Compiler von QAL ist in QAL geschrieben und übersetzt sich selbst. Ein Rust-Kern umgibt ihn.

Selbst gehostet17 Module mit rund 15 000 Zeilen QAL: Lexer, Parser, Typprüfer, Monomorphisierung, SQL-Prüfung, Kodierung und WebAssembly-Erzeugung.
Bootstrap-FixpunktStufe 1, 2 und 3 des Compilers sind byte-gleich. Das wird nach jeder Änderung am Compiler neu nachgewiesen.
Rust-ReferenzEin unabhängiger Referenzcompiler in Rust rechnet parallel; Testsuiten vergleichen beide über einen Korpus von über 900 Programmen.
Paralleles PrüfenGroße Programme werden in Arbeitspakete geteilt und auf mehreren Kernen geprüft. CHECK_DELTA prüft nur die geänderten Rümpfe gegen gespeicherte Signaturen.
Rust-KernRund 52 000 Zeilen Rust für Speicher, Laufzeit, Beweiser, Server und Werkzeuge, ohne eine einzige Compiler-Warnung.
Diagnosen

Jeder Fehler hat einen Namen

Eine Diagnose besteht aus Code, Art, Definition, Pfad, Nachricht und Hinweisen. Eine Auswahl der Codes, die ein Agent am häufigsten sieht:

Beim Schreiben

CodeBedeutung
E0201unbekannter Name
E0202Name doppelt vergeben
E0240reservierter Name, etwa aus der Prelude oder std.
E0241 · E0242SQL kein Literal oder nicht erlaubte Anweisung
E0301Effekt benutzt, aber nicht deklariert
E0404eine Definition verweist auf zwei Namen derselben Definition
E0508Effekt beim Ausführen nicht freigegeben
E0540todo() wurde ausgeführt
E0801Vertrag widerlegt; nicht gespeichert, mit Gegenbeispiel

Warnungen nach einem define

CodeBedeutung
E0803Property-Test fehlgeschlagen
E0804Property-Test löst einen Abbruch aus, etwa Überlauf oder Index
E0805ein Produkt ohne Schranke kann überlaufen
E0806Funktion geändert, aber kein Test im selben Schritt
E0807Ausgabe früherer echter Läufe hat sich geändert

Im Team

CodeBedeutung
E0901Name gehört gerade einem anderen Änderungssatz
E0905 · E0906außerhalb des Auftrags oder Schnittstelle geändert
E0910 – E0913Merge: Konflikt, passt nicht, Beweis oder Test schlägt fehl, Freigabe fehlt
Gemessen, nicht behauptet

Die Zahlen hinter der einen Runde

Alle Werte stammen aus Messungen am 25. und 26. Oktober 2026. Die Berichte liegen im Repository unter bench/.

0,28 sMedian eines vollständigen define, 66 Funktionenbench/loop/report.md
0,41–0,46 sderselbe Ablauf bei 1520 Definitionen, früher 4,5–5,0 sbench/loop/report.md
0 / 2424Abweichungen zwischen inkrementeller und vollständiger PrüfungDifferenztest, 318 Speicher
95 / 96Stufen mit allen verborgenen Tests grün, Läufe 7–14bench/living
Ein define, alle fünf PrüfungenVorherJetzt
66 Funktionen (Median)1,24 s0,28 s
1520 Definitionen4,5–5,0 s0,41–0,46 s
Tokens eines Agenten im Vergleich zu Rust2,06×1,29–1,32×
Ein echter Fang

Alle Tests grün, und trotzdem ein Fehler

Ein Haiku-Agent sollte mehrzeilige Bestellungen einbauen. Nach seinem ersten define bestanden alle seine eigenen Tests. Nur das Verhaltensgedächtnis meldete, dass eine alte, einzeilige Bestellung jetzt anders kostet.

  1. Der Agent las die Warnung und erkannte: Einzeilige Bestellungen müssen gleich bleiben.
  2. Er korrigierte die Rabattformel in der nächsten Runde.
  3. Gegenprobe: Der Stand vor der Korrektur hätte 5 von 50 verborgenen Tests verletzt.

Bei gezielt eingebauten Fehlern meldet E0807 allein, ohne einen einzigen Test, 11 von 13. In 30 Live-Versuchen gab es keinen Fehlalarm.

E0807 behaviour_changed
this define changed what `main` prints on 3 of 25 earlier runs: `OK o1 8800` is now `OK o1 8835`
Wörtlich aus Versuch 12, Commit 9ab47ae8
Warum QAL

Wenn ein Agent den Code schreibt

  • Rückmeldung in einer RundeEin Agent erfährt sofort, ob Typen, Verträge, Tests und Abhängige stimmen. Er muss keinen Build-Lauf planen und keine Logs lesen.
  • Fehler, die Tests nicht sehenBeweise und das Verhaltensgedächtnis fangen, was die eigenen Tests eines Agenten übersehen.
  • Kontrollierte WirkungJeder Effekt steht im Typ und muss freigegeben werden. Ohne --allow model kann ein Programm kein Modell aufrufen und kein Geld ausgeben.
  • Antworten als DatenJedes Ergebnis ist JSON, jeder Fehler hat einen Code, einen Pfad und einen Hinweis zur Behebung.
  • Zusammenarbeit ohne ChaosRollen, Leases, ein Merge-Tor und eine signierte Geschichte machen nachvollziehbar, welcher Agent was geändert hat.
Was noch nicht besser ist

Ehrlich gemessen

  • KostenAgenten brauchen in QAL etwa 1,3-mal so viele Tokens wie in Rust. Der größte Posten ist die Sprachreferenz, die jeder Agent mitliest.
  • Kein Zeitgewinn pro AufgabeBei kleinen Programmen ändert die schnellere Prüfung an Runden und Laufzeit messbar nichts. Ihr Nutzen zeigt sich bei großen Programmen und als Sicherheitsnetz.
  • Beweise mit GrenzenExakt sind sie für Ganzzahlen und Wahrheitswerte. Was Z3 nicht beweisen kann, wird zur Laufzeit geprüft.
  • Junge SpracheGemessen ist QAL an einem Bestellsystem mit zwölf Änderungsstufen. Breitere Erfahrung im Einsatz fehlt noch.
Loslegen

Ein Projekt, ein Speicher, die erste Runde

QAL wird mit Cargo gebaut. Agenten verbinden sich über den MCP-Server; Menschen nutzen dieselben Befehle auf der Kommandozeile.

Bauen
cargo build --release --manifest-path qal/Cargo.toml -p qal-cli
Speicher anlegen und Code schreiben
qal init && qal define konto.qal
Alle Tests laufen lassen und einen Vertrag beweisen
qal test && qal prove deposit
Für Agenten: den MCP-Server im Projekt starten
qal mcp --root .
Ein Programm als Webdienst betreiben
qal serve handle --listen 127.0.0.1:8080 --allow db