diff options
Diffstat (limited to 'doc/sphinx/language/core')
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..07dcfff444 --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,37 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter <extensions>`), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system |