On 6/8/13, Marta Bunge <martabunge@hotmail.com> wrote:
The assertion "the theory of programming languages and the field of logic can be seen as essentially identical to category theory " is pure nonsense, even more so as it is given an outrageous name - "computational trinitarianism" even if spoken in jest.
The term "computational trinitarianism" http://ncatlab.org/nlab/show/computational+trinitarianism refers to the theorem relating category theory and type theory http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theor... The further relation between type theory to logic and programming languages is similarly well established. The term "computational trinitarianism" was invented by Bob Harper in an expositional blog post http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ designed to alert an unspecialized public about these nice and useful facts. I guess that's what the author of that article about Spivak's paper picked up. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]