Sunday, February 05, 2012

The Life of an Academic, Explained

A friend who was dating a post-doctoral researcher at the MIT Media Lab once said, “Jean, please explain to me your life. I don’t understand you academics.” This post is intended for those considering relationships with academics, those thinking about becoming academics, and those bewildered family members of academics.

In this post "academic" mostly refers to "graduate student" but some of the things I say seem to apply to more senior academics (professors, researchers) as well.

How we spend our time. On a typical weekday, I wake up at some point and go into the office. Depending on my meetings and other activities, I go to yoga or for a run before or after this. I usually spent 7-10 hours in my office, depending on how much I slack off and how long it takes for me to finish my major tasks. I try not to work on weekends (at most a few hours) so I can recharge for the upcoming week. My schedule is similar to those of my friends in math/science at Harvard/MIT. Experimental scientists spend more time in lab.

My free time includes meals (which I often spend with friends), 1-2 hours each evening, and weekends. I usually spend my evenings and some part of each weekend pursuing my hobbies, which include reading, blogging, doing things related to women in tech, and a rotating other activity. I spend Friday and Saturday evenings with friends.

My MIT grad student friends have on average 1.5 serious non-research hobbies. Common hobbies include running/biking, doing outdoors activities, doing recreational programming, starting a company, and spending time with a significant other and/or children.

The social life of an academic usually depends on level of introversion. Some academics never leave their offices while others are out 3-7 nights a week. Regardless of whether they do it while socializing or in lab, academics tend to value their wind-down mechanisms.

All of this only holds during times of the year without deadlines.

Advisors. During grad school orientation, I was told that my relationship with my advisor would become more important and demanding than any other relationship in my life. This was no exaggeration. My advisor has the ability to graduate me and he has the ability to cut off my funding. While my advisor gives me a good deal of freedom about what I work on and how I structure my time, we both understand his power.

Paper deadlines. Computer science publishes mainly in conferences. In my area (programming languages), there are two top conferences and a few other highly-regarded, more specialized conferences. In my area of computer science, each conference takes submissions once a year. Acceptance rates can be as low as 15%. Conference submissions are full-length papers; small differences in presentation can make the difference between “accept” and “reject.”

During the 2-3 weeks before a deadline, it is normal for me to work 10-12 hours on weekdays and 8-10 hours on weekend days. One senior graduate student told me what makes or breaks a (computer science) grad student is their ability to “bust their butt” for a deadline. During this time he was working 80 hours a week to finish up a project.

Besides the coarse “promotion” structure (done with Ph.D. vs. not; tenured vs. not), there are many more nuanced factors that determine an academic’s status: 1) which big discoveries they have made and 2) how well they give the impression that they are making big discoveries. Some of this is measurable (for instance, through publication count and citation index) and some of it is more intangible (for instance, reputation in the community).

Fears of academics include being scooped, being wrong, fading into obscurity, and having insufficient intellectual freedom. Many academics are happy just to avoid these situations.

Life goals. We do have goals--though they may not be as concrete as you might like. We may not talk about them because they are often too lofty (for instance, winning the Nobel Prize or Turing Award) or dependent on variable factors (faculty job at a top school; starting a lucrative company) to discuss. The nature of the pressures and prospects we face, as well as the attitudes of our peers, make it highly likely that we will learn to handle a fair amount of uncertainty and risk. For these reasons it is also common for academics to have goals that depend on specific other people (and specific geographic locations) as little as possible.

Spending time with academics. If the academic in your life is willing to make you their hobby, then you can expect to spend a good deal of time with him or her with variability from paper deadlines, grant deadlines, conference and other travel, and teaching schedules. Otherwise how much you see your academic depends on how many common activities you share. Even if you are considered a good friend, this can range from a few times a week to once every few months.

What does an academic look like?
My friend Lan made the video below for a science documentary class to capture the life of a grad student. It features three MIT grad students, including me.

rocks, bands, logic (2012) from Lan Angela Li on Vimeo.

Thursday, February 02, 2012

Verve as a CACM Research Highlight

My paper with Chris Hawblitzel "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" appeared as a Research Highlight (read here) of the Communications of the Association of Computing Machinery (CACM) in December. This is a shortened version of our 2010 paper appearing at the Programming Language Design and Implementation (PLDI) conference altered for a more general audience.

This paper describes the Verve operating system, the first operating system verified end-to-end and automatically for type safety. This means that programs running in Verve cannot suffer from whole classes of memory-related errors. The main idea of Verve is to implement the operating system in a type-safe language (C#), write a specification for the memory interface between the type-safe parts and the lower-level parts (the C# code does not mess up the stack; the low-level code does not mess up the heap), and verify the low-level parts of the system (in our case, using Boogie that translates to x86 assembly).

An exciting thing is that Xavier Leroy, who is responsible for both OCaml and the CompCert verified C compiler, wrote the Technical Perspective, "Safety First!" He writes, "The formal verification of high-assurance software is making great progress lately. Yang and Hawblitzel's work, along with other recent breakthroughs in software verification such as the seL4 verified microkernel of Klein et al. (see Communications, June 2010, p. 107), were unthinkable 10 years ago. Little by little, one point at a time, these results sketch a promised land where, with mathematical certainty, software does behave properly after all."

Another exciting thing for current graduate students interested in this work is that my Microsoft Research mentor Chris Hawblitzel is looking for a summer intern to work on adding concurrency to Verve. Not only was Chris Hawblitzel amazing for helping me learn everything I needed for this project, but he was also a fun mentor. I recommend that you contact him ASAP if you are interested in working with his this summer.

Wednesday, February 01, 2012

Research Update: A Language for Automatically Enforcing Privacy Policies

For the last three years, I have been working on things building up to the creation of Jeeves (project website here), a new programming language for automatically enforcing privacy policies. Last week I presented our first paper on Jeeves at the Principles of Programming Language (POPL) conference. You may read our paper here and look over the slides here.

To describe Jeeves I will quote Jacob Aron, who does a good job in this recent New Scientist article:

Even with your friends under control, a software bug could still expose your private data - as Facebook CEO Mark Zuckerberg himself found out recently when a glitch revealed his photos to the world. To solve this, researchers at the Massachusetts Institute of Technology have come up with a new programming language called Jeeves that automatically enforces privacy policies.

Programmers have to explicitly ensure data flowing through their software obeys necessary privacy policies, but it is easy to slip up and let information leak out. Jeeves solves that by substituting the value of variables within the software depending on who the user is. For example, say Alice posts a message but doesn't want anyone but herself to see who wrote it. The programmer can use the variable "author" without worrying what the user sees - when the software runs, Jeeves ensures Alice will see her own name, but everyone else logging in will see "Anonymous".

Jean Yang, who helped develop Jeeves, says the new language lets a programmer delegate privacy responsibilities and concentrate on the actual function of their code, much like a party host might entrust their butler with ensuring the needs of each guest are met so they can spend more time socialising.

Jeeves allows the programmer to provide high-level declarative policies for privacy and rely on the runtime system to automatically produce outputs adhering to these policies. The Jeeves runtime uses symbolic evaluation and constraint-solving in order to do this. We have an implementation of Jeeves as an embedded domain-specific language in Scala. (Code here.)

Next steps for Jeeves include looking at how Jeeves can handle policies for integrity and declassification (in addition to confidentiality) and looking ta how well Jeeves scales for real-world applications.

It says a lot about our research community that languages and solvers are at a point where we can even consider this sort of separation of global concerns from core program functionality. I am excited about a future in which we can continue to make programmers’ lives easier by teasing out and automating concerns such as privacy.