Following a blog entry of David A. Wheeler I arrived to the web page of Open Proofs: http://www.openproofs.org/ he created.
In short, as I did not understand much, there are tools to mathematically prove that a certain program does something or does not do something. Unfortunately most of these tools and most of their use is secret. To quote the web site "Verified software is often highly classified, sensitive, and/or proprietary. In addition, research papers are too short and abstract to present meaningful examples." The idea behind the web site is to provide a set of open source tools and examples of open source software with proofs, that is open proofs. There is an example of a short C program with its proof http://www.openproofs.org/wiki/Queens_on_a_chessboard_with_Caduceus All this seems to be interesting but I could hardly understand it. Maybe someone here is also interested and could explain. Maybe someone could point us to tools that can prove a piece of Perl 5 or at least a piece of Perl 6 code. regards Gabor -- Gabor Szabo http://szabgab.com/blog.html Test Automation Tips http://szabgab.com/test_automation_tips.html
