Getting software right with properties, generated tests, and proofs

Evolve your hack into robust software!

If you suspend your transcription on, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!

Please do not press “publish” on to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.

Video duration
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.

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 <b>QuickCheck</b>. (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.

Talk ID
12:50 p.m.
Resilience & Sustainability
Type of
Mike Sperber
Talk Slug & media link

Talk & Speaker speed statistics

Very rough underestimation:
174.5 wpm
938.0 spm
100.0% Checking done100.0%
0.0% Syncing done0.0%
0.0% Transcribing done0.0%
0.0% Nothing done yet0.0%

Work on this video on Amara!

Talk & Speaker speed statistics with word clouds

Whole talk:
174.5 wpm
938.0 spm