Sun, 30 Oct 2005 00:00:00 UT

Ontic, Epigram - Unifying Functions and Types

Since I first mentioned Richard Hamming's You and Your Research, I've been looking for an affordable copy of the associated out-of-print book, The Art of Doing Science and Engineering : Learning to Learn. At the same time, I'm applying the advice in his speech. Roughly, "Find the most important research in your field, then do that."

One of most important computer science research topics I see right now is unifying functions and types.
My interest started when I discovered the Curry Howard isomorphism, and quickly spread to the Epigram language. Recent discussions on Lambda the Ultimate show that Michael Dummet in the philosophy community has found a similar isomorphism. Here's part of that discussion by Charles Stewart:

The link between Curry-Howard-like correspondences and the kind of philosophical logic that Michael Dummett does have been known for a long time, but not commented about recently, for a stupid reason: the link is essentially two hops between three disciplines:

The literature around the Curry-Howard correspondence links structural proof theory to theoretical computer science, but the literature tends to turn on technicalities of the lambda-calculus that tend to frighten off philosophers;

Dummett's work links structural proof theory to core theses of philosophical logic and philosophy of language, but his work and the literature around it tends to turn on such deeply metaphysical issues like the relationship of logic to the possibility of our knowing the real nature of the external world, which tends to frighten off computer scientists, theoretical or not.

So I wonder, what will happen if the existing body of theoretical work in the fields of computer science, proof theory, and philosophy are discovered to be different ways of looking at the same thing?

What do you see as the most important computer science research topics of today?

More neat quotes today:

More important, however, is that software /development/ is itself full of emergent behavior. Since software development is basically knowledge discovery, the impact of the process, the team practices, and most importantly the individuals and their interactions, makes every project different.
--Ron Jeffries

This next quote sounds like the Curry-Howard isomorphism all over again:

Since everything happens much faster these days, it should only take a few more years for management to realize that spending prodigious amounts of time and money on use cases and other specs results in the software being written twice -- once by the analyst in the form of specs and again by the programmers in the actual code.
-- Robert Watson

The results suggest the existence of a visual pathway that bypasses the primary visual cortex and can process some characteristics unconsciously, the scientists said. That's a scary thought, Basilisks and the Deep Structures trick from Snow Crash might really work.