2015-08-05T13:13:49Z Photos, electronics, cnc, and more Jeff Eplerjepler@unpythonic.net 2015-08-05T13:13:49Z 2015-08-05T13:13:49Z https://gamma.unpythonic.net/01438780429 I won a copy of the book <a href="http://hackersdelight.org/">Hacker's Delight</a> from <a href="http://blog.regehr.org/">John Regehr</a> for my entry in his <a href="http://blog.regehr.org/archives/1213">nibble sort contest</a> earlier this year. <p>In that thread I had heard about the <a href="http://www.cprover.org/cbmc/">CBMC Bounded Model Checking software</a>, 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. <p>I have a modest start on github, which I am calling &quot;Proven Delights&quot;: