We don’t know but looking into the past hints at the future. Cantor, Hilbert and Gödel gave us Church who gave us Turing. Turing and Flowers gave us the machi

We don’t know but looking into the past hints at the future. Cantor, Hilbert and Gödel gave us Church who gave us Turing. Turing and Flowers gave us the machines as well as the theory. All of them put together gave us type systems and types are how you formally prove that your 747 software is free of, if not all bugs, then at least certain large classes of error. There is a clear line of connections from Cantor (1890s) to jumbo jet fly-by-wire (1990s.) Countability of sets and Cantor’s diagonal argument — the subject of the first part of this article — are some of the first topics teenagers learn about in high school CS (if you’re lucky and on a very modern course) or CS101 (if you’re at a University.) Types are sets. Who knows what today’s mathematics will bring us in the year 2121?