All worlds but one

There have been several vastly important revolutions in human knowledge in the last hundred years or so.  Global communication changed how we see the world.  DNA and the human genome project changed how we see life.  General relativity changed how we see space and time.  But the one I'm interested in today is the one that most people don't even realize happened.  In the early 1900's there was a revolution in mathematics.  And it changed the way we see everything.  What started with the likes of Bertrand Russell, Gerhard Gentzen, and David Hilbert ended with the likes of Kurt Gödel, Alonzo Church, and Alan Turing.  Most people didn't notice a difference in the thoughts and methods of abstract, ivory tower academics.  And I doubt they would care even if it they did.  But they do notice the IDevice™ in their pocket, the computer that does their taxes, and the massive outgrowth of automation that governs more of our daily lives by the minute.

And I don't quite mean that the mathematical revolution gave us computers.  Computers were on their way regardless of what mathematics was up to.  Mathematics gave us turing completeness and lambda calculus.  I also don't quite mean that our current technological wonderland is due to turing completeness and lambda calculus.  Most of the developers responsible for our current lifestyle are only vaguely aware that such things exist.  These developers learn the bare minimum and then plow relentlessly ahead; following their imaginations.  However, imagination will only get you so far.  Eventually, overly ambitious plans must cede to the limit of human comprehension in the face of overwhelming complexity.  Mathematics, however, provides avenues to tame this complexity.  And it has been sinisterly added to even the simplest developer's toolbox.  Why the honest and practical minded developers of today would be shocked to find that they have been making use of monads and theorem provers for years.  But they have.  And our increasingly technical world would not exist if this wasn't the case.

Philip Wadler is a mathematician who has a certain interest in lambda calculus and computation.  He came up with a marvelous phrase … lambda calculus is the omniversal programming language.  You see, it might be said that lambda calculus is a universal programming language.  Being mathematics, any civilization in the universe could independently come to the same conclusions that Alonzo Church did in the 1930's.  But it goes further than that.  Because it's mathematics, it should be able to also exist in other universes.  So it is truly omniversal.

Of course, personally, I have some reservations about an omniversal programming language.  While I can't imagine the nature of a universe where mathematics does not function, I can imagine that such a place might exist.  Lambda calculus itself argues against its status as omniversal.  In lambda calculus, things are not allowed to come from nowhere.  There *are* free variables, but they are really only free in a local, constrained context.  There must be some larger scope which introduces the free variable, or else it is an absurd entity without any meaning.  If in the world of lambda calculus everything must come from somewhere, then where did lambda calculus come from.  Surely it cannot exist of its own nature by its own nature for its nature is that this cannot happen.  So it points to a world outside of itself; where it does not care to venture.