Introduction
Throughout our rich three thousand year history of mathematics, there's existed time immemorial tension between the finitely discrete and the infintely continuous descriptions of reality. That same beautiful tension is repeating itself with computation. And it's our opportunity as programmers to experience that beauty. Let's take a deeper look into what we exactly mean1.
A Discrete Hope
Taking a look at where mathematics all began, we find ourselves in the world of Ancient Greece. One way to conceptualize the Ancient Greece zeitgeist is to imagine that of Silicon Valley. Although the average programmer might have more monetary benefit to their profession, they both have access to experience the beauty of reality. In the same way a beginner programmer entering the profession possesses a childlike awe that somehow the code they express on their keyboard will lay down the bricks of the intergalactic network, so too does the novice mathematician inpsiringly wonder how the symbols they inscribe on paper reflect the astronomical stars of space.
In order to build the cathedrals and bazaars of digital reality, programmers orchestrate the tools of languages and runtimes — created for them by toolsmiths we call compiler writers and kernel engineers — in concert with one another to write programs. While the ancient greek mathematician did not have access to mechanical computation to execute the instructions of said program, they nonetheless had access to formal language — created for them by the toolsmith we call logicians — in which they were able to express proofs. The programmer uses the compiler writer's types, and the mathematicain uses the logician's propositions.2
The programmer and mathematician share a similar essence not only in the tools of type and proposition, but also in the finitely discrete nature of their intellectual creations in proof and program. That is, the programmers of the valley and the mathematicians of ancient greece share the same dream to describe and thus reduce reality with discrete language. The only minor difference is the programmer is somewhat more extreme by wanting to reduce everything down two specific integers; that of 0 and 1.
The Continuous Strikes Back
- Incommensurability of square root 2
- Sunrise Problem (of Induction)
- Probability
- Bayes Rule
Discrete vs Continuous in Computation
- Inductive Bias: Model
- Inductive Principle: Loss Function
- Empirical Risk Minimization: Maximum Likelihood Estimation
- SW1.0 and SW2.0: https://colah.github.io/posts/2015-09-NN-Types-FP/
Onward!
You have a journey ahead of you.
Are you ready to begin?
The introduction waxes and wanes philosophically with big picture metaphysics of what we can know (epistemology) and what exists (ontology) — what is coloquially known to the valley as being a wordcel. Feel free to skip to chapter 1 to get the show shape rotation on the road!
This is formally known as the Curry-Howard Correspondance.