It is a strange comment. The type theories used in programming languages, certainly in those based on the λ-cube, descend from simple type theory (via the simply-typed λ-calculus), which Russell discarded in favour of his ramified theory of types. I also wonder why Wolfram, originally a mathematician, doesn't even mention the Curry-Howard correspondence, which seems to me a fairly important result linking mathematics and computation.
No one uses ramified type theory these days, at least not that I am aware, although Russell's predicativism lives on in e.g. Feferman's programme [1] (there are some interesting results in reverse mathematics relating to this; see Simpson's book [2]).
Anyone missing the background I and the parent comment allude to might want to take a look at Thierry Coquand's article on type theory in the SEP [3]. Coquand is the originator of many ideas in this area, including the calculus of constructions [4] and the proof assistant Coq based on it.
[1] http://math.stanford.edu/~feferman/papers/predicativity.pdf
[2] http://www.math.psu.edu/simpson/sosoa/