In that thread I had heard about the CBMC Bounded Model Checking software, and it gave me the idea to combine the two: a project to take implementations of the algorithms from Hacker's Delight and prove the algorithms' properties with CBMC.
I have a modest start on github, which I am calling "Proven Delights": HTML, PDF, Source. I hope others will find the concept interesting and submit github pull requests with new proofs.
Working more with CBMC has given me a sense of why mathematicians are not fully embracing computer proofs in their work. A traditional proof, like you may have first made in high school geometry, serves two purposes: first, it shows that the desired conclusion is true in a given axiomatic system; but second, a traditional proof can be read by a fellow mathematician and lend her some abstract understanding of why the conclusion is true.
It is from that abstract understanding that she may think of some new theorem to prove. But with a so-called "proof" from software like CBMC, you only learn that the computer says the assertions in the model are not violated; there is no step by step proof process that a human can learn from. So when I have finished writing a model that I think captures the claims about the expression (x & (x-1)), and CBMC says "VERIFICATION SUCCESSFUL", I still don't understand why the expression actually "turns off the rightmost one-bit".
Still, CBMC is pretty neat. One of the proofs I wrote most recently, for
sec-ded error codes, proves in a few seconds what takes overnight with a
program to exhaustively check somewhere in excess of 2^41 distinct cases.
Not a bad speed-up!
Entry first conceived on 5 August 2015, 13:13 UTC, last modified on 5 August 2015, 14:34 UTC
Website Copyright © 2004-2024 Jeff Epler