show/hide this revision's text 2 added 17 characters in body

For the innocent observers, let me explain what joro did. He has tricked Coq into thinking that True = False is a theorem by providing an external piece of code (i.e., something that Coq does not check but simply loads into memory) that breaks Coq loading mechanism. This of course should not happen, Coq should realize that it's loading corrupted external code.

Thus, we do not have here a straight inconsistency in the Coq theorem prover, but rather a way of breaking Coq through its interaction with the external environment. There are in fact many ways in which this can be done, such as:

  1. Expose the computer to cosmic rays that cause the CPU to malfunction occasionally. (If you think this is a joke you should read what sort of ideas computer security experts have.)
  2. Coq depends on the runtime environment of the operating system and an extensive runtime library (to manipulate memory, strings, to communicate with the user, etc.) which is almost never bug-free. Any such bugs can in principle be used to make Coq think it proved something senseless.
  3. If the CPU has bugs then you cannot trust the execution of any program. (Who remembers the Intel Pentium division bug? Did it stop us from using computers?)
  4. If the compiler which was used to compile Coq has bugs, you cannot trust Coq to work correctly.

These are all valid concerns, some more than others. People put serious thought into making sure that their theorem provers work correctly. In particular, I think there is an ongoing effort to formally prove that the Coq core algorithm does what it is supposed to do. It is hard enough to deal with the core algorithm, let alone consider what happens when people start linking in external libraries.

Now to answer joro: I think you can trust Coq more than you can trust the average mathematician. The biological equivalent of what you did to Coq would be to give a mathematician an illegible photocopy of a paper with results that he relies on to prove theorems. If you want to trust your Coq code then you can take several precautions:

  1. Make sure you do not use any external libraries or experimental features. (You can syntactically check whether the Coq code links in any modules or uses certain experimental features.)
  2. Run your Coq code on several different operating systems.
  3. Run your Coq code on a computer in a vault inside a mountain to prevent cosmic rays from reaching your computer (and don't put any radioactive bananas inside the computer either).
  4. Think about what Coq is proving and see whether it makes sense. After all, your brain is not totally clueless about math and it should be able to assess what level of credence the results deserve. (If you're proving with Coq 30000 small theorems which all look alike that's a different matter. Your brain is useless then.)
  5. Ask other people to prove the same result, but do not tell them how you did it. Compare notes.

Always remember that mathematics (still) is a human activity. Even if we use machines to do it.
show/hide this revision's text 1

For the innocent observers, let me explain what joro did. He has tricked Coq into thinking that True = False is a theorem by providing an external piece of code (i.e., something that Coq does not check but simply loads into memory) that breaks Coq loading mechanism. This of course should not happen, Coq should realize that it's loading corrupted external code.

Thus, we do not have here a straight inconsistency in the Coq theorem prover, but rather a way of breaking Coq through its interaction with the external environment. There are in fact many ways in which this can be done, such as:

  1. Expose the computer to cosmic rays that cause the CPU to malfunction occasionally. (If you think this is a joke you should read what sort of ideas computer security experts have.)
  2. Coq depends on the runtime environment of the operating system and an extensive runtime library (to manipulate memory, strings, to communicate with the user, etc.) which is almost never bug-free. Any such bugs can in principle be used to make Coq think it proved something senseless.
  3. If the CPU has bugs then you cannot trust the execution of any program. (Who remembers the Intel Pentium division bug? Did it stop us from using computers?)
  4. If the compiler which was used to compile Coq has bugs, you cannot trust Coq to work correctly.

These are all valid concerns, some more than others. People put serious thought into making sure that their theorem provers work correctly. In particular, I think there is an ongoing effort to formally prove that the Coq core algorithm does what it is supposed to do. It is hard enough to deal with the core algorithm, let alone consider what happens when people start linking in external libraries.

Now to answer joro: I think you can trust Coq more than you can trust the average mathematician. The biological equivalent of what you did to Coq would be to give a mathematician an illegible photocopy of a paper with results that he relies on to prove theorems. If you want to trust your Coq code then you can take several precautions:

  1. Make sure you do not use any external libraries or experimental features. (You can syntactically check whether the Coq code links in any modules or uses certain experimental features.)
  2. Run your Coq code on several different operating systems.
  3. Run your Coq code on a computer in a vault inside a mountain to prevent cosmic rays from reaching your computer (and don't put any radioactive bananas inside the computer either).
  4. Think about what Coq is proving and see whether it makes sense. After all, your brain is not totally clueless about math and it should be able to assess what level of credence the results deserve. (If you're 30000 small theorems which all look alike that's a different matter. Your brain is useless then.)
  5. Ask other people to prove the same result, but do not tell them how you did it. Compare notes.

Always remember that mathematics (still) is a human activity. Even if we use machines to do it.