Beispielsweise richtet sich dieser Kurs in erster Linie an Studierende im ersten und zweiten Studienjahr der Ingenieur- oder Naturwissenschaften sowie an Schüler der Oberstufe und Berufstätige mit Interesse an der Programmierung. „Design by Provable Contracts“ vermittelt Ihnen, wie Sie den Schritt von „Die Tests sind bestanden“ zu „Die Mathematik besagt, dass es nicht fehlschlagen kann“ vollziehen. In fünf Modulen erklimmen Sie eine fünfstufige Beweisbarkeitsleiter – von Lint und Typen über eigenschaftsbasierte und begrenzte Modellprüfung bis hin zu abhängig typisierten Beweisen in Lean 4 –, angewendet auf ein einziges praktisches Beispiel: die Softmax-Funktion, die im modernen maschinellen Lernen verwendet wird.

Am Ende werden Sie in der Lage sein: (1) eine begutachtete wissenschaftliche Arbeit zu lesen und deren Vorbedingungen, Nachbedingungen und Invarianten in einen YAML-Vertrag zu übersetzen; (2) die richtige Verifikationsstufe für einen gegebenen Kompromiss zwischen Kosten und Konfidenz auszuwählen, unter Verwendung von Lint, Typen, Proptest und Kani in Rust; und (3) eine vollständige Pipeline vom Artikel über YAML bis hin zum Lean-Theorem aufzubauen, um eine maschinell überprüfte Garantie zu erzeugen, die für jede Eingabe beliebiger Länge gilt. Der Kurs ist praxisorientiert und tool-first: Rust für die unteren Stufen, Lean 4 für die oberste Stufe und YAML als Bindeglied zwischen Mathematik und Code. Am Ende des Kurses verfügen Sie über ein wiederverwendbares mentales Modell und ein funktionierendes Abschlussprojekt, das Sie auf jeden sicherheitskritischen numerischen Kernel anwenden können.