Isabelle is a member of the LCF family of validations, which means that you have a special module --- the output kernel — where all the outputs are executed to create the values of the thm abstract data type. This is a bit like calls to the processing system of the kernel of the operating system. All that you can create in this way is “structurally correct” regarding the correct implementation of the kernel. Since the medium of the programming language for verification (Standard ML) has very strong static properties of correctness, the correctness of building the kernel of the output is transferred to the rest of the implementation of the verification assistant, which can be quite huge.
Thus, in principle, you have a relatively small part of the "trusted kernel" and a really large "user space". In particular, most Isabelle / HOL actually represents a large collection of library theories and additional tools (mainly in SML) in the Isabelle user zone.
At Isabel, the core infrastructure is quite complex, but still very small compared to the rest of the system. The kernel is actually superimposed on the "microkernel" ( thm module ) and "nano kernel" ( Context module ). thm expresses thm values in the sense of the Milner LCF approach, and Context takes care of theory certficates for any results you produce, as well as contextual proofs for local reasoning (especially in Isar proof).
If you want to know more about LCF-style installers, I also recommend looking at HOL-Light , which is probably the smallest realistic LCF family system, realistic in the sense that people have great apps with it. HOL-Light has the great advantage that its implementation can be easily understood, but this minimalism also has some disadvantages: it does not fully protect the user from numbness in his ML environment, namely OCaml instead of SML. For various technical reasons, OCaml is by default not "safe" like standard ML.
Makarius
source share