Warum lässt sich mathematisch beweisen, dass ein Programm 100 % fehlerfrei ist – ohne es ein einziges Mal auszuführen? Die Wissenschaft der formalen Verifikation
Typtheorie und der Curry-Howard-Isomorphismus: Die tiefgründige Harmonie von Aussagen = Typen und Beweisen = Programmen