User:Boris Tsirelson/Sandbox1: Difference between revisions
imported>Boris Tsirelson No edit summary |
imported>Boris Tsirelson No edit summary |
||
| Line 1: | Line 1: | ||
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.) | 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. | |||
Revision as of 06:38, 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.