User:Boris Tsirelson/Sandbox1

Formal languages inevitably are less human readable than natural languages. However, some formal languages are less human readable than other formal languages. These are low-level languages. Being simple they are convenient for theoretical analysis and automatic processing. Being poor they are inconvenient for expressing human thoughts. To this end one needs high level languages, rich of means of expression. (This situation is observed in logic and programming as well.)

The high-level Isabelle/Isar/HOL formal language is supported by a complicated software. Such a software usually contains some bugs. However it does not mean that the proof assistant sometimes certifies wrong theorems, as explained below.

Isabelle contains a relatively small, simple, trustworthy component, the kernel. Only the kernel can certify a theorem. The kernel does not understand the high-level language, but only a low-level ("primitive") language. Other components of Isabelle translate proofs from the high-level language to the low-level language and sumbit them to the kernel. An error outside the kernel cannot force the kernel to accept a wrong proof.

Still, some doubts remain. Execution of the kernel involves a hardware, an operating system, and an implementation of a programming language. These can be buggy,corrupted by a hacker, etc.; but such scenarios are rather exotic.

A more realistic scenario is an error in the translation into the primitive language. It may happen that a (right) theorem certified by the kernel is not equivalent to a (wrong) "theorem" written and read by humans. It is also noted that the kernel is not so much small and simple as to be very trustworthy.

A higher reliability can be achieved by an independent proof checker, a very small and simple program, possibly executed on a different computer, intended solely for verification of proofs translated by a proof assistant into a low-level language. But still, this translation process escapes verification.