[SystemSafety] Correctness by Construction

[Olwen Morgan]

> 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>