Referential transparency -- whatever that means -- and the path forward.
Over the last six days I have been listening to his holiness the Dalia Lama speak. He is teaching the The Great Treatise on the Stages of the Path to Enlightenment. First, let me say, aside from having an excellent karma rating on Slashdot, I am not a practicing Buddhist and don’t purport to be any kind of expert on the teachings (in this universe anyway). I do find Buddhist teachings (at least the ones I can understand) interesting and insightful, however. Indeed, they probably would have helped with back in grad school when I was trying to get my head around quantum mechanics.
As was noted in the program guide, the Great Treatise is part of the lamrin texts, which are considered to be free of any contradictions. This single statement held my center for quite a while. The lamrim is thousands of pages of text explaining some of the most heady concepts in the world and is free of contradiction. I read this as fully self consistent. Gödel’s first incompleteness theorem not withstanding, that was probably not an easy thing to do.
Returning to world of ones and zeros, when I was new to programming, I thought, wouldn’t it be nice to automatically verify software and make sure it was free of bugs. Then I learned something interesting. Much to my horror, it is basically impossible to fully verify programs in any kind of formal way. Based on the work of Church, Gödel and Turing in the 1930s, the halting problem puts a “halt” to any such dreams. Maybe. It seems that there are formally verifiable languages based on mathematics and logic that are used to design things like flight controllers (autopilots), but I suppose at the lowest level, the programs still are running on Von-Newman architectures where absolute verification is not possible. That is, we don’t have hardware that executes logic directly. Admittedly, I’m way out my area of expertise here, so anyone with some insight please feel free to add a comment.
As you may recall, I have been talking about the Erlang language. One of the properties of functional languages, like Erlang, is something called Referential Transparency — which, by the way, it is one of those phrases that immediately makes you sound really smart at cocktail parties. In any case, referential transparency, in the context of computer programs, is a property where you can replace an existing expression with a new one and still have the program function the same as before. Of course this sounds easier than it is in practice. I am sure we all recall, “optimizing” a part of a program only to find we break some other part. This problem is very common in “procedural” or imperative programs due to destructive assignment or what I like to call the The X=X+1 Issue.
Functional programming languages, like Erlang, are declarative and are often referentially transparent. Of course, other than being a smart sounding phrase, what does “referential transparency” really mean to anyone writing code? Plenty. When a language is referentially transparent, then you can do all kinds of things to existing programs automatically and be assured you did not break them or change their behavior. What kind of things you ask? How about proving correctness, finding bugs that could not be found through testing, simplifying an algorithm, optimizing code by means of memoization, common subexpression elimination or parallelization. Ding Ding, there is that word “parallelization”.1
Here is the bottom line. Suppose you decide to write programs using Erlang (or even Haskell). Since you described what you wanted to do (and not how) in a referentially transparent manner, your program could be automatically transformed into a parallel version, or from parallel to serial, or optimized, or changed in some other way and still behave that same as you intended. (i.e. it is important to note that if your functional program computes π as 3, it can be transformed into a different functional program, but it will still compute π as 3. There is no magic here.)
The technique of automating program changes is often referred to as Refactoring. Indeed, there are efforts like Wranger and RefactorErl that can refactor Erlang programs. In fairness, refactoring is not easy. It can get complicated and all the wonderful transformations I mention above may not be currently possible with current functional languages, but it is possible. There is work to be done. And, it should be noted, such analysis is “kind of” possible with imperative languages, but functional languages provide a written guarantee of program correctness.
In closing, the point of this discussion is rather pragmatic. When the next revolution in computer hardware comes about, it may be possible for a compiler to refactor your program automatically. In the current case of procedural programs (C, C++, Fortran, etc.) and multi-core, we have no such capability. Rather, the only recourse, other than recoding, is to read rants by guys like me who are looking for a path to programming enlightenment. And where this will lead, I have no idea, but I sometimes think at the end of path there will be a door. In this door is small portal. The portal will open, and a doorman will state: Nobody gets to see the Wizard, not no body, not no how. I knew this was not going to be easy.
1 And by the way, “memoization” is another cool word to use when you are in the middle of a geek throw-down. Often best used in the following context. When some Java-boy says, So what is referential transparency good for?, you simply reply “Well, obviously, automated memoization comes immediately to mind.” Check and mate, but I digress.