> No, theorems are not scary things mathematicians do. For programmers, they’re more like unit tests, except they can involve symbols, allowing you to cover inf

> No, theorems are not scary things mathematicians do. For programmers, they’re more like unit tests, except they can involve symbols, allowing you to cover infinitely many test cases. If you like unit tests, you’ll love theorems. It's a little more complicated than that. On the one hand, it is true that a theorem can be more exhaustive than a test, but on the other hand, a test can be black box on any chosen scale while a proof cannot. While a test could assert that, foo(3) = 5 and a theorem could assert that ∀ n ∈ Nat . foo(n) = 2n-1, the test case is the same regardless of how complex foo is, while proving the theorem requires examining foo's inner workings (and changing the proof when the implementation changes), and the effort does not scale kindly with the size of foo [1]. If proving theorems were really like unit tests only stronger, we'd prove our programs all the time, where in reality, the only programs ever proven correct (with respect to some specification) using proof assistants corresponded to fewer than 10KLOC of C, took years of effort by well-trained experts, and even then required extreme simplification and a limited choice of algorithms to keep proofs manageable. Research into formal methods -- using deductive proofs written with proof assistants or many other more automated methods -- is largely if not mostly about managing what you want to know about your program with how costly it is to know it, and practitioners also make similar choices on their end. [1]: Proofs of some properties do scale well with program size, but they are special properties, called inductive invariants or composable properties (an example is memory safety, which is why it's relatively easy to show that programs written in memory-safe languages, like most high-level languages these days, are memory-safe).