[FOM] "Hidden" contradictions

[Timothy Y. Chow]

On Mon, 19 Aug 2013, Rob Arthan wrote:
> That is not true. Many computer scientists and engineers work with 
> formal machine-checked specifications and formal machine-checked proofs. 
> Donald MacKenzie's book "Mechanizing Proof: Computing, Risk, and Trust" 
> is an accessible reference with some interesting observations on this.

This is a good point that I had not considered.  Hardware or software that 
was "formally verified" to be correct but was actually wrong might be the 
closest thing to what Mark Steiner was looking for.  Still, I think that 
these examples would have the flavor of a silly bug rather than of a set 
of axioms with a subtle but unnoticed inconsistency.

Tim