Getting software right with properties, generated tests, and proofs

This talk is specifically about accessible techniques: Almost any program, function, or entity has a few interesting properties, and teasing them out will enhance your understanding of what is going on in your software. The next trick is to write out the property in your programming language. People with lots of time and budget can write down enough properties to form a complete specification of the security- and safety-critical parts of a system and prove that they hold for their system. In the talk, we'll instead focus on a dead-simple technique called QuickCheck. (Your programming language almost certainly has a QuickCheck library you can use.) QuickCheck - from the code describing the property - will automatically generate as many test cases as you want, run them, and produce counterexamples for failures. QuickCheck is amazingly effective at flushing out those corner cases that elude traditional unit tests. Finally, for simple properties of pure functions, we can also attempt a proof using simple algebra. The results are a wonderful feeling of satisfaction, and a sound sleep.