Computability, types, tests, and why flat-earthers are bad at QA
When an apple hit Newton’s head, he couldn’t prove all apples would do the same, but he could prove they wouldn’t. When we write tests, we cannot prove our code works, we can only prove it doesn’t. Types complement tests like mathematics complement physics, in this talk we’ll see why, and how.
This talk is as much of a journey through epistemology as it is a journey through software testing. How can we prove correctness is not the right question to ask. The right question to ask is: "Can we ever prove correctness?"
We’ll explore and compare the parallels between mathematics and physics, and types and tests. If physics cannot prove its theories are truthful, why do we believe it? We believe it for the same reason we believe in tests: we make observations, create models and check if reality matches our assumptions. When we have a formal system with well-defined rules, such as we have in mathematics, things change: truth is now attainable. We’ll explore the most brilliant ideas in the field of computer science and see how they can be applied to make better software, faster, with fewer bugs.
Going beyond theory, we’ll see how we can better use TypeScript’s features to make impossible states indeed impossible by using generics, conditional types, intersection and union types, discriminated unions and exhaustiveness checking and many others, after all, since TypeScript is Turing Complete, with it we can write any program that has ever been written or that will ever be written.