The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Jose Manuel Rodriguez Caballero wrote:
> Indeed, my prediction yesterday was, I quote myself: “My modest conclusion
> is that Russell O’Connor formally mimicked the Gödel-Rosser argument in Coq,
> but he did not consider the rôle of Coq in the foundation of mathematics as
> a whole”. So, I think that I understood the paper.

Rusell O'Connor clearly and explicitly stated how things stand with
his paper, yet you insist to pass value judgements that are completely
beside the point. I cannot explain this in any other way than your
trying to belittle Russell and prove to yourself your own
self-righteousness. I strongly support Russell's work and his
attitude, and find your attitude inappropriate.

Proofs done in Coq follow a standard of rigor which is an order of
magnitude above the standard of peer reviewed mathematics journals.
People who produce mechanised proofs in general have a much, much
better understanding of logic and foundations than most mathematicians
who publish papers. Your comments are out of place and couched in
ignorance.

Andrej