Begriff
Coq
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Model Checker (SPIN, NuSMV) sind "Brute Force". Sie probieren alle Zustände. Aber was, wenn die Zahl der Zustände unendlich ist? Dann brauchst du einen Theorem Beweiser (Proof Assistant). Coq ist ein Werkzeug, mit dem du mathematische Beweise schreibst. Du sagst: "Ich behaupte, $a+b = b+a$ für alle Zahlen." Coq sagt: "Beweise es." Du gibst Schritte ein ("Induktion über a..."). Coq prüft jeden Schritt. Am Ende steht: Qed. (Quod erat demonstrandum). Der Beweis ist 100% maschinell geprüft. Fehler unmöglich.
Merksatz: Ein interaktiver Theorembeweiser, der auf der Konstruktionenkalkül-Typentheorie basiert und es ermöglicht, mathematische Sätze und Software-Spezifikationen formal zu beweisen.
Der CompCert C-Compiler. Ein C-Compiler, der in Coq geschrieben und bewiesen wurde. Man hat mathematisch bewiesen: "Der Assembler-Code, der rauskommt, entspricht exakt dem C-Code, der reinging." Keine Compiler-Bugs mehr. Wird in der Luftfahrt (Airbus) und Atomkraft genutzt.
1. Gallina
Die Programmiersprache von Coq. Es ist eine extrem mächtige funktionale Sprache (wie OCaml/Haskell), aber mit Dependent Types. Man kann Code schreiben und über den Code Beweise führen – in derselben Sprache.
2. Curry-Howard Correspondence
Coq nutzt diesen Trick extrem. Ein Beweis ist ein Programm. Wenn das Programm kompiliert (typsicher ist), ist der Beweis korrekt. "Propositions as Types".
1. CoC: The Calculus of Constructions
Mathematisch basiert Coq auf dem CoC (Calculus of Constructions), erweitert um induktive Datentypen (CiC). Das ist das oberste Ende des "Lambda-Würfels". Coq erlaubt:
- Polymorphismus: Funktionen über Typen.
- Abhängige Typen: Typen, die von Werten abhängen (z.B. ein Vektor der Länge $n$).
- Type Operators: Konstruktionen wie "Ein Typ von Typen" (Universen). Diese Mächtigkeit ist nötig, um komplexe Aussagen wie den "Fundamental-Satz der Algebra" vollständig zu formalisieren.
2. Proof Scripts & Tactics (Ltac)
Man schreibt in Coq selten den Beweis-Term direkt (da er riesig wäre). Man schreibt ein Script in der Sprache Ltac.
Du gibst Befehle (Tactics) wie intros, induction, rewrite, ring.
Diese Tactics sind Programme, die den eigentlichen Beweis-Term für dich zusammenbauen. Ein modernes Coq-Feature sind automatisierte Solver (z. B. auto, lia), die einfache mathematische Probleme (Lineare Arithmetik) komplett selbstständig lösen, sodass sich der Mensch auf die "kreativen" Schritte des Beweises konzentrieren kann.
3. Extraction: Von Beweis zu Binary
Eines der "Killer-Features" für die Industrie ist die Extraction. Wenn du ein Programm in Coq schreibst (z. B. einen Sortier-Algorithmus) und beweist, dass es korrekt ist, kannst du Coq anweisen, daraus OCaml, Haskell oder Scheme Code zu generieren. Coq "löscht" dabei alle rein logischen Beweis-Teile (die zur Laufzeit nicht gebraucht werden) und behält nur die Berechnungs-Logik übrig. Das Ergebnis ist ein hocheffizientes Programm, das mathematisch garantiert bugfrei ist. Viele Security-Module in Smart Contracts oder kryptografische Bibliotheken werden heute so erstellt.
Quick-Check
Warum heißt es Coq?
Von Thierry Coquand (Erfinder). Und "Coq" ist französisch für Hahn (das nationale Symbol Frankreichs). Französischer Humor.Ist es schwer?
Extrem. Die Lernkurve ist eine vertikale Wand. Man muss Mathe-Studium-Level Logik verstehen.Vier-Farben-Satz?
Berühmt: Der erste große mathematische Beweis (2005), der komplett in Coq formalisiert wurde. Vorher gab es nur handgeschriebene Beweise mit "Lücken". Coq schloss die Lücken.