Nachdem ich die Hürde überwunden hatte, dieses Buch zu beginnen (ich brauchte eine ernsthafte Auffrischung der Mathematik), wurde es schnell zu einem meiner Lieblingsbücher. Das Programmieren in Coq macht extrem süchtig, und die Behandlung durch Software Foundation und die Konzepte von Programmiersprachen im Allgemeinen sind sehr gut gelungen.

Außerdem sollte ich darauf hinweisen, dass ich gerne Beweise und Induktionen in diesem Stil gelernt hätte (Beweise als Programme), anstatt meine trockenen, langweiligen Universitätsvorlesungen aus der Mathematikabteilung mit Bleistift- und Papierbeweisen. Stellen Sie jedoch sicher, dass Sie, wie bereits mehrmals im Buch erwähnt, die Bleistift- und Papier-Proofs ausführen können, da Coq Sie an Stellen wiegen kann, an denen Sie absolut keine Ahnung haben, was in Ihrem Proof tatsächlich vor sich geht. Skizzieren Sie Ihre Ideen für Ihre Proofs, bevor Sie sie codieren.

Die beste Einführung in die Verwendung von abhängig typisiertem Programmieren, um viele grundlegende CS zu beweisen. Beginnt von der einfachen Logik bis zur Teilbewertung in der Lambda-Rechnung.
Die Problemstellungen machen wirklich Spaß! Alle Übungen sind in Coq, fühlen Sie sich wie Sie ein Puzzlespiel lösen.

Die Übungen sind sehr schwierig und werden mit der neuesten Coq-Version (8.11, während ich dies schreibe) nicht immer auf dem neuesten Stand gehalten.