[FOM] "Hidden" contradictions
Timothy Y. Chow
tchow at alum.mit.edu
Tue Aug 20 19:18:52 EDT 2013
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.
More information about the FOM