Correctness Proofs

In the world of software development correctness proofs are akin to verification of codes in scientific computing, only a lot more low level. Down to the formal correctness of the hardware design in some cases. A research group from Australia has formally proved the correctness of an entire operating systems kernel. That is really awesome!

An interesting quote from the short write-up on their webpage:

With all the purity and strength of mathematical proof it is easy to get carried away. There is a fundamental theoretical limit of formal verification: there will always be some bottom level of assumptions about the physical world left and these assumptions have to be validated by other means. Mathematical proof is proof as long as it talks about formal concepts. It is when assumptions connect to reality where things may still fail.

Albert Einstein is quoted as saying "As far as the laws of mathematics refer to reality, they are not certain; and as far as they are certain, they do not refer to reality."

--Trustworthy Embedded Systems (ERTOS)

An important reminder for project managers enamoured of the assurance provided by the numerical test section's relatively easy to come-by answers.

Slashdot discussion of this result (standard posts misunderstanding Goedel's work included of course).