• High praise for the Lua programming language from a respected PL and runtime-systems researcher. Ramsey’s observation that the design effort surrounding Lua “could not have been done at a North American university” rings especially true.

  • John Carmack shares some thoughts on static program analysis for finding defects. The whole article is a good read, but I especially appreciated his tongue-in-cheek interpretation of Microsoft’s pricing model for their analysis tools (free in the Xbox developer kit, but very expensive in the Windows developer kit): “I read into this that Microsoft feels that game quality on the [Xbox] 360 impacts them more than application quality on Windows does.”

    Also, see this related and hilarious photo, especially if we went to grad school together. (Photo link via Pascal Cuoq.)


Dissertation advice

August 4th, 2010  |  Tags: , , ,  |  Leave a comment

I’ve been blissfully out of the grad school game for so long that I might have to start teaching boxing to bright-eyed masters students to keep them from entering a life of research. But I was recently reminded of the best advice for anyone embarking on a substantial applied research effort (especially a dissertation): build your work around a thesis statement. That is, your main point should be an objective, defensible point that your experiments and prose will support. It should also fit on a single slide in 64-point type.1

This point seems obvious (after all, schoolchildren are instructed to begin constructing a five-paragraph essay with a thesis statement; why wouldn’t adults do the same for a 200-page monograph?), but it is surprising how many junior and senior grads can’t express the central claim that their dissertation is meant to argue in a single sentence. I first encountered this advice from Olin Shivers’ web site early in my graduate career; it was a big help in focusing my work, even as my own research veered more into analysis than into runtime support as I had originally intended. (Shivers is also responsible for the greatest acknowledgements section of all time, which I’ve linked to earlier.) I was reminded of Shivers’ advice this morning when I read a nice article by his student Matt Might (now at Utah) elaborating on the benefits of a thesis statement, in which Shivers’ influence is palpable.

1 This last point is where the thesis statement that appears in the text of my dissertation falls short. Although my thesis statement is one sentence, it includes a great deal of unnecessary detail about specific mechanisms rather than their essential properties (e.g. “type-based analysis” instead of “scalable analysis”).

Research and development

April 18th, 2010  |  Tags: , ,  |  Leave a comment

Rob O’Callahan has done a lot of high-quality research and a lot of high-quality development; his thoughts on research (and, to a lesser extent, on development) are thus worth reading. The following passage should prove especially amusing if you’ve spent several years in some tiny subcorner of the discipline:

Since 1984 hundreds or thousands of papers have been written about program slicing, but in reality it is almost never used. I believe the research in this area has been completely pointless. Probably hundreds of millions of dollars have been wasted, not to mention enormous amounts of the time of very smart people. This is criminal misuse of resources.

(One wonders what current trend in programming language research we will have come to regard as “completely pointless” in 2020 or 2030.)

Whereof one cannot speak

July 15th, 2009  |  Tags: , , ,  |  2 Comments

Almost a year ago, I posted a short note about how to set Polytonic Greek in the LaTeX typesetting system, inspired by my difficulties in typesetting a chapter epigraph for my dissertation, and included with it a challenge to my readers: namely, say something clever about the (unattributed) quote I had included as an example:

οὐ γὰρ μήποτε τοῦτο δαμῇ εἶναι μὴ ἐόντα·
ἀλλὰ σὺ τῆσδ’ ἀφ’ ὁδοῦ διζήσιός εἶργε νόημα

Today, someone did. Congratulations are due to D Jagannathan, who had something clever to say both about the quote itself — which is from the work of the presocratic philosopher Parmenides of Elea — and about the perils of using LaTeX to set texts in non-Latin alphabets. Fine work!

One (imperfect) way to render the quote into English, given by John Burnet in 1892, is “For this shall never be proved, that the things that are not are; and do thou restrain thy thought from this way of inquiry.” Parmenides is either my favorite or second-favorite presocratic, and I like this quote for two reasons: first, it is remarkably Tractarian for something written around two-and-a-half millennia before Wittgenstein destroyed positivism; second, it could be read to describe logic programming or mechanical proof search.

While I was unable to resist one of the basest impulses of computer scientists (viz., quoting philosophers in an effort to distance oneself from the fact that one is essentially in an engineering discipline; see also here), this quote at least was plausibly connected to the chapter it headed. I was, however, able to resist the temptation to include this quote in its original language in the final version of my dissertation. (Indeed, the only moment of weakness I had with regard to non-English languages was in the dedication, where it seems a little indulgence is justifiable.)

On dependent types

June 24th, 2009  |  Tags: , ,  |  Leave a comment

One of the perils of computing is this: one encounters a problem that has some unappealing solutions (or partial solutions) and one or more obvious workarounds. Nevertheless, one is compelled to think about the possibility of an elegant, general solution to a class of similar problems. That happened to me this morning, and I wrote it up at Chapeau.

Computer science and plumbing

May 12th, 2009  |  Tags: , , ,  |  1 Comment

I enjoyed this comment by Marc Hamann in a discussion of MIT’s switch away from SICP for undergraduate computer science education; the whole comment is thought-provoking, but this excerpt is especially delightful:

Somewhat more facetiously, I have to suggest that maybe they are just being merciful to their students, since it seems that many people, seduced by the excitement of SICP, go on to suffer miserably in their career as API and framework plumbers, wishing that being a programmer was actually the elegant and rational process that Abelson and Sussman had made it out to be.

SICP, if read carefully and properly, presents almost an entire undergraduate computer science curriculum in a semester. It’s a shame that MIT EECS students won’t be drinking from that firehose any more. Furthermore, I have long believed that Scheme is unbeatable as a language for teaching computer scientists rather than programmers. (Although “unbeatable” implies a partial ordering: I’d guess it’s possible to argue that Haskell or an ML-family language is equally suitable.)

Multicore Erlang

January 28th, 2009  |  Tags: , , , , , , ,  |  Leave a comment

I was glad to see Ulf Wiger’s slides and talk from his DAMP 2009 tutorial on Erlang programming for multicore processors. I would have been very interested in attending DAMP, but it conflicted with the last day of VMCAI (and thus with my paper), so I wasn’t able to go in person.

  • Just in case you’re interested, I’ve posted a “web version” of my dissertation. (This version is different from what one might get on microfilm from UMI: the formatting is somewhat nicer, it is single-spaced, and it is designed to be printed two-sided.)


Mustard watches

January 23rd, 2009  |  Tags: , , ,  |  Leave a comment

It seems impossible that I haven’t already linked to Jean-Yves Girard’s pseudonymous masterwork “Mustard Watches: An Integrated Approach to Time and Food,” but it looks like I haven’t. Enjoy.

Appeals to authority

January 18th, 2009  |  Tags: , , ,  |  Leave a comment

I just won a months-old argument with a colleague. (I had, in fact forgotten that the argument had happened in the first place.) The specific term at the center of the argument and the identity of the colleague aren’t important, but the concession, which took the following form, was downright awesome: “We disagreed about the meaning of term X, but I have decided you are right because Patrick Cousot defined it the same way in his talk.”

Now that’s vindication.


August 2nd, 2008  |  Tags: , , , ,  |  Leave a comment


I recommend to everyone — but especially to my friends finishing dissertations, and doubly especially to those in Computer Science — Olin Shivers’ amazing acknowledgments section from the scsh manual, which I first encountered as a young Scheme nerd a long time ago. (Philip Greenspun’s gloss on Prof. Shivers’ acknowledgments is pretty delightful as well; scroll ahead to the second block quotation and prepare to be amazed.)


Speaking of acknowledgments, I make brief and jocular reference to the “preface paradox” in the draft preface of my dissertation. This is one of my favorite paradoxes (originally due to David C. Makinson). The basic idea is that a writer believes every individual claim in a manuscript is true (or else he or she would not have committed them to paper); however, some writers claim that their work inevitably will be found to contain some errors. As a consequence, writers are in the curious position of believing the conjunction of every claim in a book and believing the negation of the conjunction of every claim in a book. Whether or not this is irrational is — I guess — an open question with a few plausible solutions.

Soot 2.3.0

June 4th, 2008  |  Tags: , , , , ,  |  Leave a comment

Here’s a shout-out to the Sable group at McGill. They’ve just released a new version of the Soot compiler framework, which I’ve used extensively in my dissertation work. If you need to analyze or transform Java source or bytecode, I can’t recommend it highly enough.

Shortening the feedback loop

May 15th, 2008  |  Tags: , , ,  |  Leave a comment

Benjamin Pierce developed a graduate PL theory course based on TAPL. This isn’t that surprising, since TAPL is an excellent text and I suspect Pierce knows it rather well. The exciting part is that he taught the course with Coq, which is a pretty cool development. His report on the experience, “Using a Proof Assistant to Teach Programming Language Foundations, or Lambda, the Ultimate TA,” looks worth reading.

I like the general idea: interactive development in a proof assistant does for novice proof-writers what interactive development in a conventional programming language does for novice programmers. I also recall being a frustrated undergrad in my first class with a proof component precisely because it wasn’t always clear — before one handed in the assignment, that is — what constituted a good proof and what didn’t. However, Pierce rightly points out that teaching students to write formal, machine-checked proofs doesn’t necessarily help them to write informal proofs. (Also, Coq error messages aren’t always helpful feedback — but they’re at least as good as the worst feedback students get from a human on paper proofs.) I’m delighted to see this development, though — I’ve been thinking about the possible didactic benefits of proof assistants since I took non-classical logic early in grad school, and it will be interesting to see how Pierce’s work plays out in the larger CS pedagogy scene.


April 18th, 2008  |  Tags: ,  |  Leave a comment

Rob O’Callahan on rounding:

Unfortunately both [rounding towards zero and rounding away from zero] can get us into all kinds of trouble when we’re rounding values for use in graphics.

  • There’s a new version of Teyjus, an implementation of λ-Prolog.

  • Ott looks interesting.


Why Wikipedia is almost comically awesome

June 14th, 2007  |  Tags: , ,  |  2 Comments

I recently had occasion to visit this Wikipedia article about Alice ML. Alice ML extends Standard ML with a bunch of useful features, like future, typesafe persistence, and so on.

To motivate future, the wikipedia article author presents the recursive Fibonacci function:

fib 0 = 0
   | fib 1 = 1
   | fib n = fib(n-1) + fib(n-2);

The article then states that “[f]or large values of n, fib n will take a long time to compute.” No kidding; it’s exponential with n. However, Alice ML, according to the Wikipedia article, has a solution for this problem — and it’s not the one you learned in CS1. With future, the article informs us, it is possible to spawn a new thread to compute the nth Fibonacci number, thus saving time if the continuation of fib n does not need the result of fib n immediately.

The article neglects to mention that even Standard ML provides a mechanism to dramatically speed this function’s execution: the humble accumulator, whose straightforward application admits an implementation of fib that is linear with n.

Dyna: a declarative language for dynamic programming

February 12th, 2007  |  Tags:  |  Leave a comment

Dyna is a declarative language for writing weighted dynamic programs. It compiles supplied rules into C++ classes — here’s an example of Dijkstra’s algorithm. Although it seems to be targeted to natural-language processing, I can think of several applications in artificial language processing as well.

(If you really want to nerd out with the declarative programming, please see this implementation of Dijkstra’s algorithm in the interactive fiction language Inform.)

On the death of Visual Basic for the Mac

November 2nd, 2006  |  Tags:  |  2 Comments

Would you believe that Visual Basic for Applications runs in an environment that features dynamic code generation and behind-the-scenes vtable munging of C++ objects? Until I read this article, I wouldn’t have either. To be fair, what reasonable person would assume that a much-maligned macro language would be a playground for so much fun technology? Note that the dynamic compilation is strictly on PPC — the Windows version of the interpreter/VM is “tens of thousands of lines of IA-32 assembly that directly implements all of the opcodes.” Sounds like a threaded interpreter to me (as well as a maintenance nightmare).

[via daringfireball]

I haven’t yet decided

April 24th, 2006  |  Tags:  |  Leave a comment

whether Java 1.5 annotations are (from a compiler/program transformation perspective) the best thing to be added to Java in a very long time or a hideous addition to the long list of ways in which the Java platform design violates the end-to-end argument. Time will tell, I suppose.

I’m currently listening to Sonata no. 31 in A♭: II Allegro Molto from the album “Beethoven Piano Sonatas Nos 28-32” by Vladimir Ashkenazy


February 8th, 2006  |  Tags:  |  Leave a comment

This marks the second semester in a row that I have used the following illustration to explain integer overflow to my “Introduction to Programming” students:

Integer overflow


Python-based HDL

January 26th, 2006  |  Tags:  |  Leave a comment

LtU links to MyHDL, which translates from Python to Verilog. I can only assume that being able to use Python as a hardware description language absolutely demolishes Verilog in every way. The key idea is using Python generators (sort of like limited coroutines) to express hardware concurrency. If I’m not confused, it looks like generators (and coroutines) present an attractive way to describe other synchronous concurrent systems. DSP and synthesis code, for example, could use generators to deal with the multiple timescales involved in digital audio and with the state requirements of, e.g. synthesizer voices or digital filters.

I’m currently listening to Stand Up Tall from the album “Showtime” by Dizzee Rascal

Technorati Tags: ,


November 10th, 2005  |  Tags:  |  Leave a comment

I’ve been examining the video game scripting language TorqueScript lately. TorqueScript looks a lot like many other scripting languages: vaguely C-like syntax, separate namespaces for global and local variables, and untyped variables with automatic coercion to and from other types (generally, it seems, to strings). The documentation describes this latter feature by saying that TorqueScript is “type-insensitive.”

I have railed extensively on the sorts of malapropisms and misconceptions that professional programmers are wont to use when writing about types elsewhere, so I shall keep this brief. I had initially planned to write about how hilarious it was that these (extremely competent) programmers had made up a term for concepts that already had names. “Type-insensitive,” though, is a shockingly good term, as terms coined in popular discussion of type systems go.

The documentation illustrates the “type-insensitivity” of TorqueScript by showing that the literal string “1.2” is equivalent to the numeric constant 1.2. (This also, I suppose, raises questions about TorqueScript’s floating-point representation.) It would be nice if they clarified that operators were “type-insensitive,” rather than the language, but I’ll take what I can get in this arena.

As of this writing, the string “type-insensitive” only results in 557 Google hits. I modestly propose that “type-insensitive” replace the (oxy)moronic nomenclature that some languages are “dynamically typed,” which presently enjoys far greater currency.

I’m currently listening to IV. Choral — Andante con moto — Allegro maestoso from the album “Mendelssohn Symphony No. 5” by Berlin Philharmonic / Lorin Maazel

textbook oddness; Dijkstra

November 10th, 2005  |  Tags:  |  Leave a comment

I’m currently teaching an intro to Java programming course. The textbook is above average, but has a lot of bizarre extraneous material in sidebars. A discussion of the Intel FDIV bug (itself out of place in an introductory programming text) includes an indictment of customers who “didn’t really need” new chips and hadn’t considered the environmental costs of disposing of chips. There is a two-page “sidebar” on contested United States elections and the controversy over electronic voting machines. I’m all for introducing students to the ethical considerations of the computing professional as early as possible, but these digressions feel irrelevant, heavy-handed, and forced.

However, one sidebar made me smile by referring to Edsger Dijkstra as an “influential computer scientist.” That is sort of like referring to the Noahic flood as a “significant ecological event.”

Dijkstra, of course, had his hands in many important areas of computer science and was responsible for a baffling number of foundational results. I know that many of my readers are not computer scientists; you may wish to read “How do we tell truths that might hurt?” and “Go To Statement Considered Harmful” for examples of Dijkstra’s clarity and wit. (Computer scientists would do well to resolve to visit regularly the Dijkstra archive at Texas.)

I’m currently listening to Lachrimae (1604) Lachrimae Verae from the album “Dowland: Songs and Lachrimae” by Studio der frühen Musik & Thomas E. Binkley

“Dynamic typing”

September 9th, 2005  |  Tags:  |  Leave a comment

LtU has a discussion of “Static Typing Where Possible, Dynamic Typing When Needed” by Erik Meijer and Peter Drayton. This is a nice discussion of useful language features; I have argued elsewhere that the advantages of real type systems should be afforded to untyped languages wherever it is practical to do so via programming environment support.

LtU is one of the best internet fora for computer scientists, but it is downright silly how many people there persist in using the spurious term “dynamic typing.” It is high time for this madness to cease. If we are to be honest in our use of language, we shall call these “dynamically typed” languages what they are: untyped.

A type is a range of values. A typed language, in Cardelli’s magisterial formulation, is one in which variables can be ascribed nontrivial types. Note that this must be a static property! Perhaps advocates of the term “dynamic typing” mean that the type of a variable may change with assignment. Such a claim, however, is vacuously true for untyped languages — the range of values a variable may hold can always change with assignment. (This does not mean that a variable in an untyped language may be ascribed a type!) It should be clear that if the “type” of a variable may change with assignment, then the variable does not have a type at all.

To talk sensibly about types, we should follow Cardelli’s example and decouple discussion of typing from discussion of safety. I suspect that what most people mean by “dynamically typed” is “untyped but safe” — viz., an untyped language in which operations are checked at runtime to ensure that they are valid for the given operand values.

I’m currently listening to An Die Entfernte from the album “Schubert: 21 Lieder” by Dietrich Fischer-Dieskau

Silly talk

August 15th, 2005  |  Tags: ,  |  3 Comments

Mark Liberman and Brian Weatherson are both writing about “silly talk” about their disciplines — for example, asking a philosopher for a list of some of “[his] sayings.”

In my experience, once you get far enough along, just about every discipline is a veritable comedy goldmine in this regard. I recall someone asking Andrea — upon hearing that she had an academic interest in the Arthur legends — what she thought about the veracity of The Da Vinci Code. (She doesn’t remember this, though, so it may be apocryphal.) She does, in any case, regularly field questions about whether her dissertation work (on Middle English romances) has led her to compose a great deal of original fiction. My grad minor work, which was mostly in analytic philosophy, produced snickers from people who don’t consider, say, the problems of the conditional or of vague predicates to be worthy of investigation.

I have often claimed that computer science is special in this way, since computers are ubiquitous but computer scientists are not. As a result, people are confused by the presence of the word “computer” in the name of my discipline, and are inclined to assume that I have something vaguely to do with their wireless network or Start menu. (Frankly, I’m more confused by the “science” part of my discipline’s name.) I have gotten the following sorts of reactions upon disclosing the most general information about my present work:

  1. “Well, you’ll make a lot of money someday!” Perhaps (although the technology bubble remains burst). However, I am subject to the whims of the academic job market and a desire to remain in the upper Midwest. Furthermore, if money were my primary concern, it would be absolutely stupid for me to work on a Ph.D. instead of getting a job and investing for n extra years. (Personally, I’d have kept the consulting gig I had out of college, in which I made a grad student’s annual salary in a month.) This comment is by far the most common, and usually comes after someone is flummoxed by the fact that my wife, as a PhD candidate in literature, has no opinion on John Grisham’s latest.
  2. “Hey, you’ll have to help me get Word to mail merge/choose between these commodity PC parts/perform some other computer-related task that you’re not qualified to do.” Do you ask an astronomer to fix your binoculars? I have no idea how to use any interesting features of Word if the paperclip doesn’t tell me what to do (I haven’t used it since 1996 or so), and I don’t know anything about which brand of DVD burner is a “better deal.” This is not to say that I mind helping people with computer trouble when I can — I don’t — but that being a computer scientist has not initiated me into some Gnostic succession of secret knowledge about popular computing topics.
  3. “So, when you finish your Ph.D., are you going to program computers or fix them?” This is particularly unfortunate, as the person who asked me had a doctorate in another potentially-misunderstood field: German literature. (Perhaps I should have asked whether the lyrics of Rammstein or those of Die Toten Hosen compared more favorably to Goethe.) I have fixed computers for a paycheck before; it is fun for a while, but 10+ years of postsecondary education in order to enable such a career is at least minor overkill. Likewise, if I simply wanted to program computers, I could have dropped out of elementary school in order to hone my then-burgeoning AmigaBASIC skills.

Having to field silly questions, though, has made me much more careful to avoid this behavior myself. Erring on the side of caution has a pleasant side effect: instead of forcing people to discuss their work in social situations, I can confine the conversation to avocational topics. (After all, what would you rather talk about?) On a positive note, the preponderance of “silly talk” when nonspecialists discuss academic disciplines should serve as a wake-up call to academics: there are many levels at which we can discuss our work, and the burden is on us to make what we do clear, relevant, and accessible to laypersons.

If you have a good story about an entertaining misconception relating to your discipline (and I am certain that some regular readers do), feel free to drop it in the comments.