Non-Obfuscated Unprovable Programs & Many Resultant Subtleties
The \emph{International Obfuscated C Code Contest} was a programming contest for the most creatively obfuscated yet succinct C code. By \emph{contrast}, an interest herein is in programs which are, \emph{in a sense}, \emph{easily} seen to be correct, but which can\emph{not} be proved correct in pre-...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2016-04-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1634/pdf |
| _version_ | 1797268669683728384 |
|---|---|
| author | John Case Michael Ralston |
| author_facet | John Case Michael Ralston |
| author_sort | John Case |
| collection | DOAJ |
| description | The \emph{International Obfuscated C Code Contest} was a programming contest
for the most creatively obfuscated yet succinct C code. By \emph{contrast}, an
interest herein is in programs which are, \emph{in a sense}, \emph{easily} seen
to be correct, but which can\emph{not} be proved correct in pre-assigned,
computably axiomatized, powerful, true theories {\bf T}. A point made by our
first theorem, then, is that, then, \emph{un}verifiable programs need
\emph{not} be obfuscated!
The first theorem and its proof is followed by a motivated, concrete example
based on a remark of Hilary Putnam.
The first theorem has some non-constructivity in its statement and proof, and
the second theorem implies some of the non-constructivity is inherent. That
result, then, brings up the question of whether there is an acceptable
programming system (numbering) for which some non-constructivity of the first
theorem disappears. The third theorem shows this is the case, but for a subtle
reason explained in the text. This latter theorem has a number of corollaries,
regarding its acceptable programming system, and providing some surprises and
subtleties about proving its program properties (including universality, and
the presence of the composition control structure). The next two theorems
provide acceptable systems with contrasting surprises regarding proving
universality in them. Finally the next and last theorem (the most difficult to
prove in the paper) provides an acceptable system with some positive and
negative surprises regarding verification of its true program properties: the
existence of the control structure composition is provable for it, but anything
about true I/O-program equivalence for syntactically unequal programs is not
provable. |
| first_indexed | 2024-04-25T01:36:09Z |
| format | Article |
| id | doaj.art-f6260cb53b1b4d74aecbddd37d3fb79d |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:09Z |
| publishDate | 2016-04-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-f6260cb53b1b4d74aecbddd37d3fb79d2024-03-08T09:43:58ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742016-04-01Volume 12, Issue 210.2168/LMCS-12(2:2)20161634Non-Obfuscated Unprovable Programs & Many Resultant SubtletiesJohn CaseMichael RalstonThe \emph{International Obfuscated C Code Contest} was a programming contest for the most creatively obfuscated yet succinct C code. By \emph{contrast}, an interest herein is in programs which are, \emph{in a sense}, \emph{easily} seen to be correct, but which can\emph{not} be proved correct in pre-assigned, computably axiomatized, powerful, true theories {\bf T}. A point made by our first theorem, then, is that, then, \emph{un}verifiable programs need \emph{not} be obfuscated! The first theorem and its proof is followed by a motivated, concrete example based on a remark of Hilary Putnam. The first theorem has some non-constructivity in its statement and proof, and the second theorem implies some of the non-constructivity is inherent. That result, then, brings up the question of whether there is an acceptable programming system (numbering) for which some non-constructivity of the first theorem disappears. The third theorem shows this is the case, but for a subtle reason explained in the text. This latter theorem has a number of corollaries, regarding its acceptable programming system, and providing some surprises and subtleties about proving its program properties (including universality, and the presence of the composition control structure). The next two theorems provide acceptable systems with contrasting surprises regarding proving universality in them. Finally the next and last theorem (the most difficult to prove in the paper) provides an acceptable system with some positive and negative surprises regarding verification of its true program properties: the existence of the control structure composition is provable for it, but anything about true I/O-program equivalence for syntactically unequal programs is not provable.https://lmcs.episciences.org/1634/pdfmathematics - logiccomputer science - logic in computer sciencef.1.1f.1.3f.3.1f.4.1 |
| spellingShingle | John Case Michael Ralston Non-Obfuscated Unprovable Programs & Many Resultant Subtleties Logical Methods in Computer Science mathematics - logic computer science - logic in computer science f.1.1 f.1.3 f.3.1 f.4.1 |
| title | Non-Obfuscated Unprovable Programs & Many Resultant Subtleties |
| title_full | Non-Obfuscated Unprovable Programs & Many Resultant Subtleties |
| title_fullStr | Non-Obfuscated Unprovable Programs & Many Resultant Subtleties |
| title_full_unstemmed | Non-Obfuscated Unprovable Programs & Many Resultant Subtleties |
| title_short | Non-Obfuscated Unprovable Programs & Many Resultant Subtleties |
| title_sort | non obfuscated unprovable programs many resultant subtleties |
| topic | mathematics - logic computer science - logic in computer science f.1.1 f.1.3 f.3.1 f.4.1 |
| url | https://lmcs.episciences.org/1634/pdf |
| work_keys_str_mv | AT johncase nonobfuscatedunprovableprogramsmanyresultantsubtleties AT michaelralston nonobfuscatedunprovableprogramsmanyresultantsubtleties |