the original type theories, before they got co-opted by the CS rabble.
They are the same type theory! I realize you are at least partially joking, but it's worth noting.
Lambda calculus[0] came out of Church's studies[1] in the Foundations of Mathematics - the same field Russell was working on with his Logicism approach. Haskell Curry co-discovered the Curry–Howard correspondence which shows the direct relationship between computer programs and mathematical proofs.
Russell himself developed the idea of Type Hierarchy[2]
They are the same type theory! I realize you are at least partially joking, but it's worth noting.
Lambda calculus[0] came out of Church's studies[1] in the Foundations of Mathematics - the same field Russell was working on with his Logicism approach. Haskell Curry co-discovered the Curry–Howard correspondence which shows the direct relationship between computer programs and mathematical proofs.
Russell himself developed the idea of Type Hierarchy[2]
[0]https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
[1] https://en.wikipedia.org/wiki/Type_theory
[2] https://en.wikipedia.org/wiki/Logicism#A_solution_to_impredi...