<div dir="ltr">On Mon, Jan 11, 2016 at 6:33 PM, Lars O <span dir="ltr"><<a href="mailto:noreply@z505.com" target="_blank">noreply@z505.com</a>></span> wrote:<br><br>> ... To prove a program correct, such as Microsoft Windows and all it's dll's, would require super amounts of time, which is >not possible in this particular universe...<br>>If we develop the ability to live for 1000 years it may be possible to prove an entire operating system correct,...<br>>Correctness proving only works on trivial Toy programs that have an IN and OUT, like an old standard pascal program that just<br>
calculates things and finishes...<br>> You can only prove trivial things like 1+1=2 ...<br><br>Concerning formal methods to check whether a piece of code and even hardware is correct you could check the last milestones of at least one of the Open Source Industry-Level Automated Theorem Provers achievements:<br><br><div><div class="gmail_extra"><div class="gmail_quote"><a href="http://vstte.inf.ethz.ch/pdfs/vstte-moore-position.pdf">http://vstte.inf.ethz.ch/pdfs/vstte-moore-position.pdf</a><br><a href="https://www.cs.utexas.edu/users/moore/publications/talks/machines-2015.pdf">https://www.cs.utexas.edu/users/moore/publications/talks/machines-2015.pdf</a> </div><div class="gmail_quote"><br><br></div></div></div></div>