[Oberon] Use of resources.

[Pablo Cayuela]

On Mon, Jan 11, 2016 at 6:33 PM, Lars O <noreply at z505.com> wrote:

> ... 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...
>If we develop the ability to live for 1000 years it may be possible to
prove an entire operating system correct,...
>Correctness proving only works on trivial Toy programs that have an IN and
OUT, like an old standard pascal program that just
calculates things and finishes...
> You can only prove trivial things like 1+1=2 ...

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:

http://vstte.inf.ethz.ch/pdfs/vstte-moore-position.pdf
https://www.cs.utexas.edu/users/moore/publications/talks/machines-2015.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.inf.ethz.ch/pipermail/oberon/attachments/20160130/782053a8/attachment.html>