User:Boris Tsirelson/Sandbox1: Difference between revisions
imported>Boris Tsirelson No edit summary |
imported>Boris Tsirelson No edit summary |
||
| Line 10: | Line 10: | ||
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. | 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. | ||
A human author, interacting with the proof assistant, creates a new theory on top of old theories, typically created by others. In contrast to the proof assistant, the author usually does not investigate scrupulously all the definitions in the old theories. Rather, the new author assumes that its predecssors did not deviate unadvertently from the mathematical traditions. This is another potential source of errors: the theorem meant by the author can differ from the theorem certified by ''`Isabelle.'' | |||
Revision as of 06:56, 20 August 2010
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.
A human author, interacting with the proof assistant, creates a new theory on top of old theories, typically created by others. In contrast to the proof assistant, the author usually does not investigate scrupulously all the definitions in the old theories. Rather, the new author assumes that its predecssors did not deviate unadvertently from the mathematical traditions. This is another potential source of errors: the theorem meant by the author can differ from the theorem certified by `Isabelle.