<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<br>
<blockquote type="cite"
cite="mid:2cb6206d-70d2-1ddb-f071-310c32a2f067@phaedsys.com">It's
not obvious to me
that it is even theoretically possible.</blockquote>
<br>
<p>A whimsical thought-provoker on this theoretical possibility:
Below is a quine, a program that does not read any external file
but nevertheless prints its own source text.</p>
<p><br>
</p>
<p> <font face="Courier New, Courier, monospace">eval s="print
'eval s=';p s"</font></p>
<p><font face="Courier New, Courier, monospace"><br>
</font></p>
<p>This quine is in Ruby. I don't know of any quines in C or Ada.
Though one may think a prover might have its work cut out to prove
that this is a quine, it ought, in principle, to be easy - if only
because because the prover has to read the text of the program in
order to construct the proof.</p>
<p>In many areas of proof, lack of referential transparency can
cause big problems - but curiously not, AFAI can see, with quines.</p>
<p><br>
</p>
<p>... discuss ... (or, on second thoughts, perhaps not :-)<br>
</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<p><br>
</p>
</body>
</html>