The Coq mailing list

["dhr. dr. J McKinna" <J.McKinna AT cs.ru.nl>]

Dear Georgi,

the question

> > how a client should check a Coq proof for cheating?

touches on the difficult question of trust in the behaviour of a proof 
assistant (PA).

Let me try to add *nothing* further to the discussion than to draw your 
attention to Randy Pollack's (1997)
"How to Believe a Machine-Checked Proof",
and a companion piece from (2010) by my colleague Freek Wiedijk, entitled
"Pollack inconsistency",
which draws on Randy's ideas to focus attention on the parsing and 
pretty-printing layers of a PA, and define various ways in which most, 
but not all, PAs fail in similar ways to those you have described. In 
particular, as your examples demonstrate, Wiedijk shows that Coq is, in 
his terms, weakly Pollack-super-inconsistent (to be sure: a mouthful, 
but at least there is a name for the phenomenon).

To summarise Randy's article (and thereby do it a great injustice: I am 
constantly surprised by how little-known it is, and how seldom cited; it 
really *should* be read by anyone serious about this business): absolute 
certainty is surely unachievable, and the best one can do is take the 
sceptical view, and write one's own checker for the PA's kernel 
language. That people have not, typically, chosen to do so, ought to be 
neither here nor there.

Best wishes,

James McKinna
Radboud Universiteit Nijmegen








> > [rest of discussion deleted...]