[SystemSafety] Correctness by Construction
Olwen Morgan
olwen at phaedsys.com
Wed Jul 15 18:08:40 CEST 2020
> It's not obvious to me that it is even theoretically possible.
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.
eval s="print 'eval s=';p s"
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.
In many areas of proof, lack of referential transparency can cause big
problems - but curiously not, AFAI can see, with quines.
... discuss ... (or, on second thoughts, perhaps not :-)
Olwen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200715/d376cb03/attachment-0001.html>
More information about the systemsafety
mailing list