Greetings from Auckland, NZ where I have five hours to kill awaiting a long flight back home to Seattle—seems like a great time to respond to Lee Spector’s request that I post something to this web site. Excuse the ramble.
I graduated from Hampshire in 2000 (F96) with a Div II that was a bit of a grab bag of topics in math, physics and computer science and a Div III on resolution-based automated theorem provers. I ended up taking a lot of courses at UMass, Smith and even one at Mt. Holyoke, but many of my most stimulating classes were at Hampshire. The ones I remember best were a first-year class taught by Lee that introduced me to functional programming in Lisp and also C programming at roughly the same time; a course by David Kelly in the School of Natural Science that gave me a taste of programming in basic, matlab, and mathematica; and several courses/independent studies with Herb Bernstein and Lee on quantum computing. These classes set me off on a career in computer science research that has, so far, been a lot of fun.
I now work at Microsoft Research (MSR), a lab of about 350 full-time researchers in Redmond, and about the same number at various other sites around the world. I came to MSR from the University of Maryland, College Park where I received my Ph.D. in 2008 from the Department of Computer Science. Broadly, I research ways to develop software systems more reliably, usually in a style that provides proofs that programs meet their formal specifications.
For a flavor of some of this work, recall that many programming languages allow programmers to state lightweight specifications using types, and tools often check these specifications before compiling your program. For example, most C compilers complain that the statement (int x = “hello”) violates the specification that x always holds an integer. A lot of my work looks at how more advanced type systems can be can be used to state and prove much more precise program properties, e.g., we could define a type nat to be {x:int | x >= 0}, the type of natural numbers; the type prime could be something like {x:nat | forall y. x mod y = 0 implies y=x \/ y=1}, the type of prime numbers; or even types like {f:file | Alice CanRead f}, for the type of file handles f on which the user Alice holds the CanRead privilege. When tools can automatically check these richer specifications, programs can be accompanied by proofs that they never crash, never corrupt files, never release sensitive information on a network connection, and even that they always terminate after some finite number of steps. Of course, such program properties are undecidable in general, but many common programs do not exhibit the pathological behavior for undecidability to be an obstacle.
You can read more about some of my work at http://research.microsoft.com/~nswamy and play around with one of my programming languages on the web at http://rise4fun.com/fine. I’m always on the look out for talented students and interns. So, get in touch if you’re interested.
I look back on my time at Hampshire with slightly mixed feelings. I certainly found the close interaction with the faculty to be very stimulating and good preparation for many aspects of a career in research. I took several semesters of 2 and 3-person classes where the topic each semester was chosen by the students. Hampshire’s free-form classes got me interested and let me explore various parts of math and CS at my own pace. While teaching undergraduate classes elsewhere, I have often thought that I would never have enjoyed the structured programming assignments that I was required to give out, and that I would probably have chosen another discipline if I was to have been subject to such a curriculum. So, in this regard, Hampshire was great!
However, it has also become clear to me that to gain from Hampshire, one had to be self-motivated to an extent that is probably unreasonable for many undergraduates. While I had fantastic interactions with many of the faculty and the students, I’m saddened by the disproportionate number of unproductive interactions that I had while there. I met too many distracted people, too many who seemed to exploit the Hampshire’s freedom to get by while doing very little actual work, too many for whom the Div III was an undeserved luxury.
Even for those who were self-driven enough to direct their own studies, I wonder if spending an entire year exclusively on a single Div III project is a worthwhile use of an undergraduate’s time. I spent my year on an obscure corner of resolution-based theorem proving, and despite well-intentioned advice from my mentors, this was a year spent on a rather barren bit of research. I think I would have have gained much more by spending just a couple of months on a senior-year project, while still taking a full coarse load. In other words, while I realize that this is probably blasphemous in Hampshire circles that cherish the Div III, I think most students would be much better served if Hampshire were to adopt a more traditional model of an honors thesis, available to those that have completed 2/3 of their Div II with some level of distinction.
Anyway, so there you go. Happy 2011 to all of you!
-Nik
