Robert Harper 2013
Holy Trinity: A Scientific Discovery is TRUE if fulfills:
- Proof Theory Logic
- Algebraic Category Theory
- Program Type Theory
A Program is an ABSTRACT Mathematical Object (“M”) :
“A is true” written as “M A”,
ie M is of Type A.
Note: Program M is not about “Coding”.
[Left] : Proof Theory Logic
[Right] : Category Theory
(Video 15:30 mins)
Type Theory is the theory of construction of programming language:
Higher Order Function <=> Exponential Type
Struct, Tuple <=> Cartesian Product Type
Choices of classes of data <=> ‘Some’ Type
Logic is an application of Type Theory
Logic is a part of Math which is a part of Computer Science in which Type Theory is the ‘Theory of Construction’ of Programming Languages.