Of all the features ever introduced into programming languages, surely the ability to insert natural-language comments is the worst thought out.
Think about it: have you ever seen a comment of more than one line that wasn't out-of-date by the time you read it? Or, if the comment was more-or-less accurate, one that didn't at least contain distracting misspellings and mispunctuations?
An ideal programming language would let you write all comments in the language itself, so that the compiler could verify that comments are properly structured and consistent with the code they describe.
Now I realize this post is appearing just a few days after April 1st, but I'm not entirely joking. Static type checking is, in effect, a system of compiler-checked comments. Type checking, of course, has a role in avoiding errors—and I do find that I do make type errors that the compiler flags, and I appreciate the ability to correct those errors before runtime. But far more often than the compiler finds a type error in my code, I read the type annotations I've made, because from day to day I tend to forget the types I'm working with at any given point in the code. That is, type annotations—like pretty much everything else in programming language source code—are best thought of as more for human consumption than for the compiler.
One reason I enjoy working with Scala more than Haskell is precisely what many people consider to be a flaw in Scala, namely that Scala can't do type inference in many places where Haskell can. Scala code is consequently littered with type annotations in places where Haskell would omit them—but that means I don't have to look very far to be reminded what anything is. As with natural language, redundancy may take up more space or time in transmission, but if not overdone it's a great aid to comprehension.
I've written some Python, and I enjoy the speed and concision with which you can whip up some code when you don't have to bother with type annotations. But it's not a language I would use for code I planned to work on for a long time, or to share with other people; I don't think I could keep the types clear in my head long enough. Unless, of course, I wrote some natural-language comments to remind me. But then I'd really want the compiler to make sure those comments didn't get out of date.
I'm still looking forward to the compiler that will complain when I write a comment that says “here is an implementation of quicksort” when what I've actually coded is bubblesort. But perhaps, a few years from now, someone will announce such a thing. On April 1st.
I mostly agree with your post, however I think there will always be a place for human language comments in a programming language no matter how advanced statically checked specifications/types you can write for your functions. A dependently typed language like Idris makes it easier to write much more detailed statically checked specifications for your functions than Haskell or Scala. For example, although it won't let you write that your function should must implement quicksort, it let's you specify that the result shall be an ordered permutation of the input. If you on top of that add some way to specify statically checked runtime and memory complexity of a function (I don't know any language that let's you do this though), you can come pretty close to specifying that a function indeed implements quicksort, or at least some type of sorting with the same runtime and memory complexity.
ReplyDeleteAll right, I concede that there is no practical way to eliminate the need for human-language comments from computer languages. The software philosophers at c2.com have already hashed out this more thoroughly than I hope I will ever need to at http://c2.com/cgi/wiki?CommentCostsAndBenefits.
DeletePerhaps compilations could randomly print out warnings once in a while, with a message that points to a comment asking "Is this still true?". I'll bet the comment would be out-of-date a large fraction of the time. I'll also bet the human using the compiler would be annoyed an even larger fraction of the time.
Meanwhile, thanks for pointer to Idris. I've spent my spare time the last couple of days looking through the manual. I'm still a little baffled by the whole proof-assistant approach to programming languages, coming from the just-make-it-work software tradition rather than the mathematical one. And I'm trying to wrap my head around how the Idris-style type-theory-based approach to dependent types relates to the Eiffel-style contracts approach, which strikes me as more intuitive.