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