It blows my mind that Russell invented (formalized) types. Such an elemental concept, but so useful.
Russell’s types aren’t really the same notion as types in programming: https://planetmath.org/russellstheoryoftypes
alt Hacker News
Russell’s types aren’t really the same notion as types in programming: https://planetmath.org/russellstheoryoftypes