In 1980 the Introduction to Computer Science course at the University of Maryland was redesigned; it changed from being a fairly easy “Heeeeere’s FORTRAN!” cream-puff to a killer filter course intended to weed out the uncommitted and/or clueless from a program that had become popular with students looking for the Big Money, which was supposed to be in computer software in those days. The redesign made it lots harder, a mix of practical programming experience and theory. You couldn’t pass it without doing (A) a difficult project (at least for students who’d presumably never programmed before) and (B) running a mathematical gauntlet erected by a guy named Harlan Mills.
He was famous (we were told). He’d taken on some tough projects in the IBM Federal Systems Division and completed them under budget and under time, using some then radical development methodologies. And he was going to teach us how to program! We should feel lucky (I recall them actually saying this).
Anyway, the intent of the redesigned course was to deliver moderately seasoned, data-structure-ready students to a more advanced curriculum, rather than just doing the traditional Large Cow College practice of running them through FORTRAN/punch-card hell in the first year, teaching them Pascal in the second, and doing data structures sometime in the third. A worthwhile endeavor, yes.
Class began. First lecture, generic CS professor: “Here’s Pascal. It’s got control structures and records and stuff. Here’s a sorting routine.” Some students were terrified at this point. I was going through the Pascal text figuring out where you had to put semicolons and how badly broken strings really were in the language (ans: lots). I’d been programming in assembly for years, and had learned C the previous year, and had mucked around with other languages and systems, so Pascal was no big deal. Ho hum.
Second lecture, Harlan: “Taking this loop, we prove by induction that it computes the sum of the first ten integers. Here are a bunch of logic formulas (lots of scribbles on the overhead). Here’s a notation you’re supposed to use, it’s got CONJUNCTION and DISJUNCTION and COMPOSITION and SO FORTH. By inference [and some hand-waving] this five line program computes some squares, yes?”
Class: Huh? Not even panic, just a collective, bug-eyed “What the fuck??”
First quiz: We had to evaluate the CONJUNCTION and DISJUNCTION and COMPOSITION mysteries against some symbols that didn’t make any sense. Plus, we answered some silly questions about Pascal. First quiz, I got like 60%. Well, you got to throw out some low quiz scores.
The rest of the semester ping-ponged like this: A perfectly reasonable killer filter course in programming (scanners, parsers, expression analyzers, etc.) alternated with borderline psychotic pseudo-math that revolved around “proving” that itty bitty programs were doing what they should. The pass rate on the mid-term was miserable; the questions were Harlan-heavy and practically everyone failed the exam. I recall the profs berating the class for doing poorly (and the teaching assistants told us that Mills was “really upset.”) Then the profs apologized and Harlan give a kind of “here’s what I really mean” come-to-Jesus lecture during which we finally got what he was driving at. It was pretty darned cool. You could almost see the little light-bulbs popping on over people’s heads as enlightenment struck us, one by one –
“Yup, he’s trying to fuck us.”
The fact that the Harlan half of the course wasn’t working didn’t mean that things were rosy in the traditional “wipe them out with programming assignments” half; not many students were finishing the projects, and since each project built upon the functionality of the prior one you were screwed if you flubbed your earlier efforts. The class was getting smaller every week. At one point I think they gave the class an implementation of a scanner to help out the students who were irretrievably behind. My impression was that they were in trouble with the administration because of the class drop rate.
I was having fun. All of my projects worked. In my spare time I was going through a bunch of stuff on LISP (Allen’s Anatomy of LISP and a copy of The LISP Machine Manual that my friend Jack had given me). It lined up really well, and I considered my extra-curricular reading my real CS education that semester.
The final project was, of course, a toy calculator for doing Mills’ CONJUNCTION and DISJUNCTION stuff over a set of symbols. When they drew the curtain and revealed this project, I just said “fuck it,” wrote most of a simple LISP interpreter in Pascal, and then wrote the “calculator” in that. Correct level of abstraction, right?
In the last lecture before the final exam someone asked “Did anyone finish the final project?”
“Yes, one person did, but they used a really elaborate structure. Um, are they here?”
I sensed that, while I’d finished the damned thing, the instructors hadn’t liked my solution very much. I didn’t raise my hand.
Forward 25 years. I’ve learned a lot about proofs, but probably more about impossible killer assignments. I had worse (much, much worse) teachers; Mills at least wanted us do good work in an area he clearly enjoyed. I have worked on projects where I’ve wished there were proofs about functionality; I’ve stared at ten lines of code for days trying to figure out if the code was correct (async stuff is fun). (Mills didn’t get into asynchronicity, I think our heads would have exploded).
But Joe Programmer is not a logician and will never persuaded to perform induction on loops and so forth because his boss is yelling at him to get that web page for Finance working yesterday, why are you screwing around with all that math?
Program proving is just becoming mainstream, but not in the sense that Harlan appeared to have wanted. Proving large, interesting programs correct is still just too hard, and will probably be extremely hard for any interesting value of “interesting” (proofs have been done for some operating systems and languages, but these are major efforts on nearly toy systems, and are probably about as much fun to work with as unextended Pascal — but are you going to prove, say, the game-save logic for Halo correct?).
But if it’s not in the compiler or editor, it doesn’t matter. It’s secondary to the the work that people focus on unless there is an economic incentive to get things absolutely correct.
There are inferencing tools now that do a lot more static checking against annotated code than we were able to do in the bad old 80s. Style checkers and “idiom enforcers” are also available for languages like C# and Java. These are what Joe Programmer needs; tools that help make designs and code better, that spot security problems and errors early in development, that continue to work as systems mature, and that can be easily integrated into the development cycle.
Whatever misfavors Harlan did for his students, he meant well, and I appreciate his goals (if not his methods) every time I crack open a large, large hunk of code and try to figure out what it’s doing.