Have you ever wondered what it takes to prove something? In this class, we will talk about proof thinking, different kinds of proofs, and work with small examples in a real-world theorem prover! Even though proofs are a mathematical tool, this class will introduce proofs in a computer science setting, in particular proving properties of a piece of code. NO experience required with proofs, code, math, or anything else :)

After writing your perfect program, you suddenly find out it has a mysterious bug. You trace the program line by line, run dozens of tests, and realize it's unclear what the code was supposed to do in the first place. Does this sound familiar? Introducing: formal verification! With formal verification, you can ensure that your program has the desired properties without writing a single test. No more frustration over missing edge cases, unclear program descriptions, and changing every line of code just-barely-so in hopes to find and fix the bug at random. Formal verification is here to help, and it can be automated, too. Dafny is a web-based automated verification tool that allows you to write your program directly in a web browser, specify very clear constraints (using assert statements and loop invariants, among other things), and run the verifier. If your code adheres to the constraints, Dafny will finish with 0 errors. However, if Dafny finds an issue, the line of buggy code will be underlined. The tool and the tutorial are available online completely free, so you could keep experimenting even after class is over. The class will be taught as a short introduction followed by hands-on exercises in Dafny, no set up required. Change your life and discover formal verification today!