Getting software right with properties, generated tests, and proofs

(Evolve your hack into robust software!) How do we write software that works - or rather, how do we ensure it's correct once it's written? We can just try it out and run it, and see if it works on a few examples. If the program was correct to begin with, that's great - but if it's not, we're going to miss bugs. Bugs that might crash our computer, make it vulnerable to attacks, stop the factory, endanger lives, or "just" leave us unsatisfied. This talk is about techniques every programmer can use to avoid large classes of bugs. You think about general properties of the things in your code, verify them through automatically generated tests, and (when it's particularly critical) proofs. This is a surprisingly fun and satisfying experience, and any programmer can do it. You need just a bit of high school math (which we'll refresh in the talk) to get started.