Das Programm Coq ist ein Beweis-Assistent, der algebraische Sätze behandeln, Beweise mit diesen Sätzen prüfen und ein zertifiziertes Programm aus dem konstruktiven Beweis seiner formalen Spezifikation extrahieren kann. (non)