Monday, March 28, 2011

Computational Trinitarianism

Given that software is so utterly confusing, it's often helpful to bring in metaphors from other areas, Christianity in this case: The Holy Trinity from Bob Harper's excellent Existential Type:
The Christian doctrine of trinitarianism states that there is one God that is manifest in three persons, the Father, the Son, and the Holy Spirit, who together form the Holy Trinity. The doctrine of computational trinitarianism holds that computation manifests itself in three forms: proofs of propositions, programs of a type, and mappings between structures. These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures. The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

1 comment:

Tony said...

I hoped you might write 'otherwise excellent' ...

The issues of incompressible biologicals only rarely impede the evangelical narrative. His arguments to them in his blog are, "it's what we do", i.e., emulate him in his servant-supported work, and "it's fun", i.e., take pleasure in perks of supported absorption.

Unfortunately for students, the perks and supports may appear to be bounded in time and bounded to long before their retirements. Which is why CMU's official statement on the new curriculum claims the new curriculum will support a 50+ year career after graduation -- an economic argument.

( which would be strengthened, don't you think, if CMU funded some support for ML libraries? )