Why Is A Math Proof Like A Unit Test?

by Daniela Wellisz

In her talk titled "Why Is A Math Proof Like A Unit Test?", Daniela Wellisz explores the parallels between mathematical proofs and unit testing in software development. She begins by drawing connections between the two fields, suggesting that both disciplines rely on specific logical principles and structured proofs or tests to establish truth or correctness. Daniela, who transitioned from a background in mathematics to programming, highlights her journey into Test-Driven Development (TDD) and how this method resonated with her mathematical thinking. She provides a humorous anecdote about the differing approaches of mathematicians, engineers, and physicists to problem-solving, implying that mathematicians often focus on conceptual solutions rather than practical ones.

Key points discussed include:

- The definition and importance of mathematical induction, where one proves a statement for all integers by validating it for a base case (typically 1) and proving it holds true for n and n+1.

- An explanation of summation notation and its relevance to understanding mathematical properties, illustrating this with the classic problem of summing the first n integers.

- Anecdotes about Carl Friedrich Gauss to contextualize mathematical concepts and engage the audience.

- The contrast between mathematical proofs and unit tests, emphasizing that tests in programming serve heuristic functions rather than definitive proofs of correctness.

- The importance of heuristics in both mathematics and programming, particularly in breaking complex problems into manageable parts.

By the end of her talk, Daniela underscores the distinction between testing and proving, advocating for a deeper comprehension of these concepts in software development. Her conclusion emphasizes that, much like mathematical proofs, unit tests do not guarantee that a code behaves as intended in every circumstance. Instead, they serve as guides, allowing developers to understand and clarify the problems they aim to solve. This insight serves as an encouragement for individuals with a strong mathematical background to consider agile development practices in their programming endeavors.

00:00:08.240 Welcome to our penultimate talk of the day. I love that word! Our speaker is Daniela Wellisz. She has a fan club! I met Daniela when we were both working at Pivotal Labs, and she is now at Cher's Post. She studied math in college and today she will talk to you about the equivalence theorem between testing and math proofs.

00:00:49.600 Hi everyone! The title of my talk is "Why Is a Math Proof Like a Unit Test?" I picked this title because it reminds me of a quote by the mathematician Charles Dodgson: "Why is a raven like a writing desk?" If you recognize that riddle, it's because it's from Alice in Wonderland, and Dodgson is indeed Lewis Carroll. The original mock riddle didn’t have an answer, but perhaps this question will! Let me first share a bit about myself. My name is Daniela Wellisz, as Josh mentioned. I've only been programming for about a year and a half. Before that, and since I was very young, I knew that I wanted to be a mathematician.

00:01:40.880 Here's what I love about math. I’m the girl on the right saying, "Oh hey, I didn't see you guys all the way over there!" Mathematicians live in a world that's based on concepts, which they build using a defined set of logical principles. They don't need to think about the world of science or reality because they are off in their own little world. There's a joke about a mathematician, an engineer, and a physicist who all get stuck in a burning motel room. One night, the engineer wakes up, sees that his hotel room's on fire, notices there’s a bucket and a faucet, so he starts filling buckets with water and pouring them on the fire until it goes out. Then, he goes back to sleep.

00:02:15.840 The next night, the physicist wakes up, sees that his motel room's on fire, calculates exactly how much water he needs to put on the fire for it to go out, pours that much water on the fire, and then goes back to sleep. The third night, the mathematician wakes up, sees that his room's on fire, looks at the bucket, looks at the faucet, and says, "Ah, a solution exists," and goes back to sleep. This demonstrates that mathematicians dwell in the world of concept, and they don’t need to care about the actual solution to a problem, just the context of it.

00:03:11.680 So, I was studying math and loving it until I realized that academia wasn't for me. I ran off with my BA to find what I could do that I enjoyed as much. That's when I went to a RailsBridge workshop. Many of you have probably heard about RailsBridge; it's a day-and-a-half workshop that aims to get underrepresented groups into Rails. I met mentors there who were agile developers and convinced me to start using Test-Driven Development (TDD) immediately. Thus, I began testing from pretty much the ground up, and quickly found an agile job that I loved.

00:03:43.840 The fact that this transition happened so quickly made me wonder what it was about TDD that made me so happy and made me love what I was doing, reminiscent of how I felt while studying math. One day, I was coding with a pair and we came across a nifty recursive problem that's even more fun in Ruby with all those lopsided methods. We ended up transforming a hash of hashes into an array of arrays. After we finished our implementation and story and started running rake, we got to talking.

00:04:20.000 Now, my pair hadn't studied any math formally; he actually majored in dance! He was curious if I had encountered much recursion during my math studies. Of course, I had studied recursion; math is indeed filled with recursion. So, recursion itself is a mathematical concept based on something called induction.

00:05:25.840 Side note: for the purposes of this talk, when I say induction, I mean mathematical induction. When I say integer, I'll only mention positive integers. If you're laughing, you probably care about this distinction, and if you’re not laughing, then you don't have to worry about it. Let's talk about induction! Induction is a way of proving properties about integers. First, you show that a property is true for one, and then you show that if it is true for an arbitrary integer n, then it must also be true for n plus one.

00:05:56.480 As you may have noticed from some of the liberties I've taken in my proof, induction is not actually possible in our spec, but I will get back to that later. After we discuss induction a bit more, when you prove something is true for n plus one based on it being true for n, you're essentially stating that if it's true for one, then it's true for two. If it’s true for two, it's true for three, thus recursively being true for every integer.

00:06:43.440 There are some methods in my mock proof—or mock test—that I haven't defined yet, so let's talk about them for a moment. How many of you remember studying or learning summation notation? Lots of hands but some people aren’t raising theirs. Sorry, I got sidetracked by mail. Anyway, summation notation, sometimes called sigma notation, is a mathematical loop where you add up whatever is to the right of the sigma, which is the zigzag Greek letter.

00:07:14.000 You start with where you are and where you're using the variable at the bottom of the sigma and at the top you have the upper bound. I put a Ruby implementation there; you might wonder why I'm using recursion instead of inject, but I mentioned recursion, so I’m using recursion. What are we trying to prove? We’re trying to show that the sum of the first n numbers is n times (n plus one) over two. This is one of the classic problems in number theory and is one of the first things students solve when learning induction for the first time.

00:08:31.200 The first person to encounter this probably started by idly adding up numbers and then noticed this property emerge. So they wondered if this happens for every integer. You can convince yourself it works if you look at two triangles, each of which has a number of dots equal to the sum of the first seven integers. If you combine the triangles, you’ll get a rectangle with a number of dots equal to twice the number of dots in either triangle.

00:09:05.920 For example, you can consider a rectangle with seven columns and eight rows. Hence, the number of dots is seven times eight, meaning the number of dots in either triangle is half of that. There's a story that accompanies this property about the mathematician Carl Friedrich Gauss. When he was a young boy, he was a very precocious child and would annoy his teacher by solving problems put to him immediately.

00:10:02.880 One day, to try to shut him up for a bit, his teacher asked him to add up the first hundred numbers. Before his teacher could even take a breath, Gauss shouted out, "5050!" He understood intuitively that the sum of the first hundred numbers is 100 times 101 divided by 2.

00:10:35.680 Now that we have established what we are trying to prove, let's perform induction. We start by checking if this holds for the sum of the first one numbers. The sum of the first one numbers is just one, which is half of 2, so that works. The next step is to assume that it’s true for some arbitrary integer n. Assuming it’s true for n, we want to show that it’s true for n plus one—that is, the sum of the first n plus one numbers is (n plus one) times (n plus two) over two.

00:11:13.680 Let’s look at the sum of the first n plus one numbers, which is really just (n plus one) plus the sum of the first n numbers. This expression representing the sum of the first n numbers has emerged again, so we can replace that with our assumption. We still have a failing test because, even though we have (n plus one) plus n times (n plus one) over two—which looks close to what we want—we lack a computer here to do the necessary steps for us. I mean, yes, there's a computer, but... so we have to keep iterating until we get green.

00:12:12.480 Then, the sum of the first n plus one numbers turns into two times (n plus one) over two plus n times (n plus one) over two. You can now combine those, rearranging the addition order to get n times (n plus one) plus two times (n plus one) over two. We’re close but need to check if we have reached the target we're aiming for.

00:12:49.600 To do that, we pull out (n plus two) and get (n plus two) times (n plus one) over two. If we rearrange that, then we confirm we have proven that this property holds for all integers, because it's true in general for some arbitrary integer n plus one, given that it's true for some arbitrary integer.

00:13:29.680 Let’s take a little break. We’ve successfully proven this property, and there was much rejoicing! But why doesn’t this work in our spec? Let’s go back to our mock proof. If you look at that line where it says n equals integer.new, something strange happens: we get a no method error regarding this method integer.new. We cannot create an arbitrary integer, so this test does not compile and fails. To get past this line, we have to do something impossible.

00:14:19.440 So, why is this impossible? And why do we even need this impossible step in the first place? Let's examine what makes it impossible. If you want to do this in our spec, you can choose specific integers; for instance, you may choose seven and say it works for seven- therefore, it should also work for eight. But that doesn't establish that it holds for all numbers. Even if you loop through 20 numbers and verify this for 20 instances, you still cannot confirm it works for an arbitrary context-less number.

00:14:55.440 Additionally, picking random numbers doesn’t hold up because a random number doesn’t equate to any number. Showing that it works for random numbers only proves that it holds for numbers filtered through your random number generator. So why do we need a context-less number at all? The different concepts of integers in programming versus mathematics play a critical role here.

00:15:24.560 As programmers, we build integers one way, and mathematicians construct them using axioms, which may seem trivial but are essential to establish any system. One axiom asserts that zero exists. Therefore, within the mathematical source code of integers, there’s the axiom of induction, stating that if you have a set S that contains zero and if it has some integer n in it, then n plus one is also included in that set. Therefore, that set is essentially the integers.

00:15:56.960 In constructing integers through finite RAM, it’s not feasible to assume the ability to have systems that operate recursively and indefinitely. You may have heard the phrase "everything in Ruby is an object." This means everything is an instance of something. For instance, seven is a specific instance of an integer, bringing along specific properties—it's prime, it's one more than six, and one less than eight, while also being a cube...

00:16:58.080 So, you can’t allow seven to represent any number. The same issue arises when writing specs. I know many will argue that we have classes that can be defined and initialized, allowing us to say class.get.new and get an instance that symbolizes anything. However, that does not mean you lack special cases. For example, if you have a unit test for a method called 'eat mushroom' for a user named Alice, it might behave differently for Alice than for Bob.

00:17:22.560 Hence, your test suite isn't a proof that your code works. It's crucial to grasp what function it genuinely serves. Unit tests function as heuristics rather than proofs. Heuristics serve to study methodologies and the rules of discovery and invention. Mathematician George Polya, who wrote a book called 'How to Solve It,' aimed to revive heuristics in a modern and modest format.

00:18:00.880 Polya emphasizes that it's unwise to answer a question you don't understand—it's unfortunate to work toward an end you don't desire. Thus, before you tackle a problem, one must comprehend it fully. In test-driven development, you often start with your integration test, ensuring you know the problem you aim to solve because you will write a test that fails if it doesn’t work.

00:18:48.560 Another point he makes, although misattributed, is: if you can’t resolve a problem, there exists an easier problem you cannot solve. This statement means you should break problems into manageable segments until you reach the simplest one and the easiest to address.

00:19:46.720 We also experience this; test failures guide our next steps. Heuristics are invaluable in navigating our problems. Polya urged the importance of distinguishing between heuristics and proofs. They’re equally valid but serve different purposes, just like scaffolding when erecting a building.

00:20:51.680 While taking time off from college, I tutored math to inner-city kids in Los Angeles, where the school district is notoriously lacking. The teachers often didn't fully grasp the material they were teaching, making it difficult for students to comprehend what they were expected to learn. Thankfully, I had a firm grasp of understanding mathematical systems from my own studies, which made it easier for me to explain things to students in relatable terms.

00:21:31.600 My understanding of axioms provided me with the tools necessary for effective communication about mathematical concepts, such as adding fractions. Similarly, recognizing the difference between a test suite and a proof is vital. First, it helps you articulate your methods to others while test-driving. It also allows you to identify the gap between testing and proving, particularly in understanding that full test coverage doesn’t imply that your test suite is proven.

00:22:25.120 In conclusion, resolving tasks in small segments is more logical and mathematical. Use this to logically analyze the process it takes to prove something. Test-driven development serves as a beneficial tool for mathematically inclined minds. If you have a friend who's highly mathematically minded and wants to learn coding, I would recommend agile practices to them.

00:23:20.000 Moreover, understanding the heuristics surrounding this subject enhances our capacity to impart knowledge effectively. Thank you!

00:25:12.240 Does anyone have any questions?

00:25:38.640 What would you describe as the axioms of software development?

00:26:04.320 That’s an interesting question. With software development, you have a computer at hand to build using code, which inherently works within the confines of being a Turing machine. Therefore, it's crucial to have an implicit understanding of your boundaries and what those boundaries entail.

00:26:39.040 I'm sure I could think of more, but that sounds like a great topic for discussion tonight at the party. Any other questions?

00:26:48.400 Okay, great! Thank you very much, Daniela.