{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:05Z","timestamp":1753889765220,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,4,20]],"date-time":"2016-04-20T00:00:00Z","timestamp":1461110400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The \\emph{International Obfuscated C Code Contest} was a programming contest\nfor the most creatively obfuscated yet succinct C code. By \\emph{contrast}, an\ninterest herein is in programs which are, \\emph{in a sense}, \\emph{easily} seen\nto be correct, but which can\\emph{not} be proved correct in pre-assigned,\ncomputably axiomatized, powerful, true theories {\\bf T}. A point made by our\nfirst theorem, then, is that, then, \\emph{un}verifiable programs need\n\\emph{not} be obfuscated!\n  The first theorem and its proof is followed by a motivated, concrete example\nbased on a remark of Hilary Putnam.\n  The first theorem has some non-constructivity in its statement and proof, and\nthe second theorem implies some of the non-constructivity is inherent. That\nresult, then, brings up the question of whether there is an acceptable\nprogramming system (numbering) for which some non-constructivity of the first\ntheorem disappears. The third theorem shows this is the case, but for a subtle\nreason explained in the text. This latter theorem has a number of corollaries,\nregarding its acceptable programming system, and providing some surprises and\nsubtleties about proving its program properties (including universality, and\nthe presence of the composition control structure). The next two theorems\nprovide acceptable systems with contrasting surprises regarding proving\nuniversality in them. Finally the next and last theorem (the most difficult to\nprove in the paper) provides an acceptable system with some positive and\nnegative surprises regarding verification of its true program properties: the\nexistence of the control structure composition is provable for it, but anything\nabout true I\/O-program equivalence for syntactically unequal programs is not\nprovable.<\/jats:p>","DOI":"10.2168\/lmcs-12(2:2)2016","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:47:33Z","timestamp":1479736053000},"source":"Crossref","is-referenced-by-count":0,"title":["Non-Obfuscated Unprovable Programs &amp; Many Resultant Subtleties"],"prefix":"10.46298","volume":"Volume 12, Issue 2","author":[{"given":"John","family":"Case","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Ralston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2016,4,20]]},"reference":[{"key":"1173:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1634\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1634\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:08:34Z","timestamp":1681243714000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1634"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,20]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(2:2)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1603.09300","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1603.09300","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2016,4,20]]},"article-number":"1634"}}