diff options
| author | narboux | 2004-04-30 15:46:06 +0000 |
|---|---|---|
| committer | narboux | 2004-04-30 15:46:06 +0000 |
| commit | f0421bd4b35c5321f90d5f31bd144394ef01a7fc (patch) | |
| tree | 9042033906dab5ad6eb4d23b4ea2c06a474c061e | |
| parent | 5b04201f606cfb6167d7f38af52622d1271e6303 (diff) | |
une question de plus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8567 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/newfaq/main.tex | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 55299d90b2..422356c0c0 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -198,6 +198,19 @@ relatively small proof-checker at the kernel of \Coq (8000 lines of ML code). Even \Coq decision procedures are producing proofs which are double-checked by the kernel. +\Question{Who do I have to trust when I see a proof checked by Coq ?} + +You have to trust : + +\begin{description} +\item[The theory behind Coq] The proof of constitency is quite complicated. You can check the papers. +\item[The Coq kernel implementation] You have to trust that the implementation of the Coq kernel mirrors the theory behind Coq. +\item[The Objective Caml compiler] The Coq kernel is writen using the Objective Caml langage, if the compiler contains a bug, Coq may prove False. The Coq kernel does not use every Ocaml features. (no object, no label ...) +\item[Your hardware] In theory, if your hardware does not work properly, Coq can prove False. +You can check your proof using different computers if you feel the need to. +\item[Your axioms] Your axioms must be consistant with the theory behind Coq. +\end{description} + \Question{Where can I find information about the theory behind \Coq ?} \begin{description} |