Lambda the Ultimate

I feel that the most important PL related areas are:

• New forms of compiler optimization
• New kinds of static program analysis Coverity style
• Dependent types
• STM
• New kinds of memory management (region inference perhaps?)

Though actually I'm not sure about the last one. GC is probably good enough these days.

That said, I'm not terribly surprised enrollments are falling. My own CS course, at Durham university in England, is everything it should not have been IMHO. And Durham is a well respected university (it's in the league below Oxbridge).

Specifically vast amounts of extremely esoteric theory and zero practical skills. Some people like that, and others argue that CS shouldn't teach practical skills, but the overwhelming opinion of the student body here seems to be that it went way too far off the beaten track. We have debts we are expected to pay off and having little or no employable skills at the end of it just isn't acceptable. Not our conditions - the banks.

For instance the lecturers here have taught propositional SAT three times now (they don't appear to communicate at all), yet have not actually covered manual memory management, not even mentioned it in passing. This is true even though they had a whole module on C++! I think it's sad that constraint solving is allowed to take a whole year yet the basics of malloc and free are not taught .... that algorithms which require a million processors to sort a thousand numbers need to be learned but the stack is still mysterious.

This results in graduates who can do clause resolution on paper but aren't able to handle any real world C/C++ codebase, which despite the flaws of that language is what a lot of useful and important software is written in. Even Java can prove a challenge. So people end up demoralised and questioning whether a career in software is for them - of all my friends on the course, I'm the only one who wants to become a computer programmer. The rest are heading either into IT departments, network administration or some non-computing related field entirely.

If asked whether I'd recommend doing computer science at Durham, I'd definitely say no, especially with the fee increases that are coming through lately. It's not financially worth it, especially as even employers like Google are wising up and often don't require a degree.

I find the most interesting research in programming languages (PL) to be the idea of melding human-computer interaction (HCI) principles with PL design, or at the very least, taking into consideration the act of programming itself when considering what must be specified in a program. What aspects of a full program specification can be relaxed and still provide a useful environment to get your work done in? How does one think about programming problems? Why is it so difficult for people to write a program for seemingly simple algorithms?

For example, I am working on a programming environment for experimenting with formal languages. When I talk to those who might want to make use of it (that collection is not a large collection, but nevertheless...) they are decidedly uninterested in two aspects of programming: data type specification and dealing with errors. Both of these tasks come across as "pointless busywork", that is, they distract the user too much from the ultimate goal of writing a program that executes the work desired. Unsurprisingly, they are also uninterested in speed of execution (at first, anyway). They want to easily express their thoughts in a programmatic fashion and see something happening quickly. Note the latter: they prefer getting to the stage of "seeing meaningful work being done" in short order over having the work itself being done in short order. In short, "the less I have to do, the better".

Facilitating that and allowing for specialization in the future is, to me at least, a very interesting challenge.

Well, CNN/Money says that the top job is software engineering (and #2 is being a college professor), and CS enrollment is dropping? Perhaps enrollment should drop. Everybody agrees that you can't add more doctors as easily as you'd like to. Perhaps we can't have this many CS majors, either?

I think the theory/practice balance will be taken care of by an inevitable change to six or seven year programs.

My late friend Ken Anderson loved to reduce the size of code to its barest essentials. He did that with algorithms too. The result was incredibly elegant. So I have found that focus on programming languages to increase expressive power fits very nicely with the desire to find better algorithms. Saying more with less also helps with a new generation that wants its socks blown off.

In my last year of undergraduate studies at the University of Toronto, I had the privilege of attending Prof. E.C.R. Hehner's course Formal Methods of Software Design. The textbook used for the course was Hehner's own A Practical Theory of Programming, which is freely available for download.

To put it bluntly, this course completely transformed the way I think about mathematics and computer science. For almost three decades, Hehner has been doing innovative research on the area of formal methods and programming languages. One breakthrough this has resulted in is Unified Algebra, a single algebra that includes what are commonly called boolean algebra, number algebra, sets, lists, functions, quantification, type theory, and limits. These forms of mathematics are the foundation of much of computer science, and Hehner brings together concepts and notations that have evolved over centuries under one consistent umbrella.

UA is the basis of aPToP, and allows aPToP to be far more expressive and easier to apply than other theories of programming such as Hoare's Logic, Dijkstra's weakest precondition predicate transformer, Back's Refinement Calculus, and Jones's Vienna Development Method. From the book's introduction:

The theory in this book is simpler than any of those just mentioned. In it, a specification is just a boolean expression. Refinement is just ordinary implication. This theory is also more general than those just mentioned, applying to both terminating and nonterminating computation, to both sequential and parallel computation, to both stand-alone and interactive computation. All at the same time, we can have variables whose initial and final values are all that is of interest, variables whose values are continually of interest, variables whose values are known only probabilistically, and variables that account for time and space. They all fit together in one theory whose basis is the standard scientific practice of writing a specification as a boolean expression whose (nonlocal) variables are whatever is considered to be of interest.

Like most well-written books, aPToP is extremely dense. Hehner provides simple, precise, formal explanations of concepts that are usually explained in round-a-bout and informal manners. For example, his formulation of "Proof by induction" is especially eye-opening; it doesn't require any special notation or format. Some of the ideas presented in just a few pages required several re-readings and took me days to properly absorb. Fortunately, I was able to attend weekly office hours with Hehner (usually one-on-one), which immensely clarified my understanding of the material.

I highly recommend all of Hehner's papers to anyone studying mathematics or computer science; I definitely feel his work represents some of the most important and interesting CS research at the moment, from a PL perspective. As Graydon mentioned before on LtU, there is room for significant work to be done developing an appropriate user interface, along with tools, to help programmers efficiently develop and maintain programs using aPToP. This kind of work could very well result in dramatic improvements in our ability to create reliable, correct software.

For my money I would say that PL-related research with a tool flavour is underappreciated whereas type-theoretic research is overhyped and gets way too much attention (sort of like high-ernergy particle physics within physics). For one thing, although many tools need some theory, too, as a rule tool-motivated theory (at least in the papers I have read) tends not to get out of hand whereas type-motivated theory does (a wild understatement). When asked how he'd pick a language for work, no less than Donald Knuth answered he'd go for the one with the best tools, not the most elegant one. Yet tools are seen as engineering stuff and are comparatively under-researched in academia; at least that is my impression. For examples of tools-flavored, not theory-drenched work that I like see, e.g, the PLT and Fluid groups. For the same reason I find some areas of security research (e.g., capabilities) very appealing: on the capabilities list participants strive to reason in plain english, they don't rush to write 10 pages of equations and type judgements. They try to be rigorous yet accessible and practical.

Transactional memory is fascinating, too, and could have a huge impact: it could be to concurrency as GC was to memory management (I don't see message-passing becoming the dominant concurrency paradigm: it would be a revolution, whereas STM is more of an evolution, albeit a potent one).

Last but not least, at the risk of being something of an heretic on this forum, I will also say that while all of the above has a PL angle (it being what Ehud asked for), I often find research on PLs per se rather boring.

I would guess CS enrolment corresponds with economic prospects for CS graduates. In my CS experience I recall very few students (and in some cases professors) seriously interested in CS, actual theoretical work. The curriculum was dumbed down, not quite to point of being "built almost entirely around the mastery of Java" (Chazelle), but pretty close, it was definitely oriented toward vocation. I noticed among some professors an uncritical acceptence and sometimes promotion of Microsoft and the use of their software in course work, and as examples for study. One professor was actually handing out copies of the student version of the Microsoft compiler.

For someone who is a serious student, I wouldn't recomend a CS education or career. Mediocrity seems to be norm in both pedagogy and real world practice. As far as programming language research, I don't see any kind of widely accepted objective research program, a kind of yard stick by which to measure the signifigance of work and progress of the field as a whole. Maybe this exists for some individual researchers, but rarely is it spelled out explicitly. It is much more common to encounter a kind of postmodernist philosophy of "everything is equally valid". It is true, that some forms of progress are clear such as the advance in the efficiency of functional languages implemented on commodity machines. However, such notions of progress have to be put in the context of progress of the field in whole (I would include machine architeture, and the expression of solutions to contemporary problems), the notion of which I think is quite lacking.

I'd say the most interesting work in Programming Languages is around proof carrying code and related areas such as software verification. The potential for these techniques are huge. Imagine for example an operating system which only installs device drivers which comes with a proof that they are working correctly. This dream is not that far off as Microsoft now has a tool for verifying certain safety properties of device drivers. A termination checker for device drivers is in the making.

This technology has the potential of solving problems of reliance, security, efficiency and of course general software correctness. I guess I'm starting to sound like a car salesman but I really believe in this technology. But there is a lot of work to be done before we can reap the benefits.