Almost two months ago, my colleagues in the Northeastern PRL wrote about three of our POPL 2017 Student Research Competition submissions. There was fourth submission, but because I was hard at work completing proofs, it wasn’t announced.

Toward Type-Preserving Compilation of Coq

Toward Type-Preserving Compilation of Coq
William J. Bowman
2016

A type-preserving compiler guarantees that a well-typed source program is compiled to a well-typed target program. Type-preserving compilation can support correctness guarantees about compilers, and optimizations in compiler intermediate languages (ILs). For instance, Morrisett et al. (1998) use type-preserving compilation from System F to a Typed Assembly Languages (TAL) to guarantee absence of stuckness, even when linking with arbitrary (well-typed) TAL code. Tarditi et al. (1996) develop a compiler for ML that uses a typed IL for optimizations.

We develop type-preserving closure conversion for the Calculus of Constructions (CC). Typed closure conversion has been studied for simply-typed languages (Minamide1996, Ahmed2008, New2016) and polymorphic languages (Minamide1996, Morrisett1998). Dependent types introduce new challenges to both typed closure conversion in particular and to type preservation proofs in general.

Full disclosure: This blog post is sponsored in part by ACM SIGPLAN. ACM SIGPLAN! Pushing the envelope of language abstractions for making programs better, faster, correcter, stronger.

TLDR

I went to ICFP again this year. I’m a frequent attendee. Last year I had a paper and gave a talk. This year I had a paper, but someone else gave the talk. But I also gave a talk at HOPE 2016. I met some people and saw some talks and pet a deer.

I returned from ECOOP a few weeks ago, and have been trying to figure out what I got of the experience. I’ll focus on two big things.

For a long time I have been debating what I should do after I graduate, which I usually phrase as “industry vs academia”. I’m coming to understand this is a false dichotomy, as most dichotomies are. (It helps that a friend spelled it out for me.) Dave Herman’s talk, on starting and running a research lab doing academic-style work (e.g., developing a principled, safe programming language) in industry, helped me see that. Shriram’s summer school lectures were equally helpful, and sort of the dual of this: taking objects from industry—scripting languages—and applying academic rigor to them. ECOOP, more than any other conference I’ve been to, brought together industry and academia in a smooth spectrum. I wish I had attended as a younger student.

The other big thing was a crystallized version of thoughts I had on programming language. Matthias Felleisen on Racket and Larry Wall on Perl 6 helped me see this: anything you might want to do to or in a program should be expressible in your programming language (Matthias said it better). This is what annoys me about languages like C, Java, and Coq. C has the preprocessor and make and the dynamic linker, etc. Java has Eclipse. Coq has OCaml plugins. All of these languages require doing “more” than writing programs, but have no way to express it in the language. Racket (and, apparently, Perl 6) pulls those things into the language so that those too become just writing programs: extend the reader, dynamically load a library, muck about with the top level, add new syntax.

I got a handful of smaller things: insights about what objects are best at, what a long-term (~25 year) research agenda looks like, an appreciation for the 99 different designs for any given program.

ECOOP was a great experience. If I go again, though, I hope the summer school won’t conflict with the entire research track.

Full disclosure: This blog post is sponsored and required by the National Science Foundation (NSF): The NSF! Funding SCIENCE! since 1683 or whenever.

TLDR

I’m going to ECOOP to see a part of the PL community I wouldn’t normally see, talk to people that I wouldn’t normally talk to, attend the co-located summer school, and figure out what I want to do with my (academic) life. If you want to know why I might do those things, read a little about me.

The long story

On Sunday, I am heading to ECOOP. I have never been to ECOOP, the conference is a little outside of my specialty, I do not know anyone there, and I do not even have a paper or talk at one of the workshops. However, a few weeks ago I ignored an email from one of the mailing lists that said there was some NSF funding that students should apply for. Then I saw an email from Jan Vitek on a local mailing list saying students should really apply for this funding and get to go to Rome.

“Huh”, I thought to myself, “I wonder what’s interesting in Rome”. I went to the ECOOP program and started looking around.

The Curry On program looks interesting. This co-located conference should help me understand how PL applies to industry problems. Unfortunately, I’m going to miss most or all the first day. But the talk I’m most interested in is the final keynote, “Building an Open Source Research Lab”; hopefully this will give me some insights on this industry vs academia problem I have been struggling with.

There is also a summer school. While the history of typed and untyped languages looks fascinating, I’m going to have to skip part of it to learn about type specialization of JavaScript programs; I prove things on type-preserving compilation and I want to see more work that uses types for optimizations. Next up, the lecture on “Building a Research Program for Scripting Languages” should help me better understand what an academic career will look like, and give me some idea of how to be a good academic. Then I’m going to learn how to build a JIT compiler for free, because despite being a compilers expert, I don’t know anything about JIT compilers. Finally, I’m going to learn a little about experimental evaluation; I normally do theory and proofs, but I imagine one day I might need to measure something.

Unfortunately, the summer school is in parallel with most of the conference talks, so it’s going to be tough to decide how much of the summer school to miss in order to see new research.

“Yeah”, I thought after much consideration, “I guess there are some interesting things to see in Rome”. I’m a little concerned about the accommodations and venue though; I understand that a lot of the architecture in Rome is very old.

I recently¹, finally, got a smart phone—an iPhone. One of the first things that annoyed me were the ads. I use Ad-Block Plus on all my computers and I have not been bothered by ads in quite some time.

One approach to removing ads is rooting my phone and installing a customized hosts file. This approach has several flaws. I once tried this approach on my android tablet. While better than nothing, it misses many ads and tends to interrupt normal internet use.

Another approach, as of iOS 9, is to use Safari content filters. However, this requires me to use Safari, and I prefer Firefox.

After lots of tinkering and reading and thinking, the best approach seems to be a VPN with proxy that seamlessly block ads (and potentially provide additional security, privacy, caching, and etc). There are apps that provide a VPN with ad blocking proxy, but reading their privacy policies caused me great concern. So I decided to setup my own.

I have not posted in a while. I have been busy starting to focus on what my dissertation topic will be. This has brought on lots of thinking about the future, including whether or not I want to go into academia. I used to be sure, but I have become less sure…

When I started doing research, I thought to myself “Ah, the freedom to set my own schedule, work on interesting problems, and not worry about whether or not my work is directly increasing profits!”. I think this is largely true… of graduate students. But the more I am in academia, the more concerned I am that professors have no such luxuries.

Professors seem to spend an inordinate amount of time on things other than research: teaching, preparing to teach, grading assignments of those being taught, applying for money, sitting on committees, reviewing applications, scheduling talks, scheduling visitors, reviewing papers, and so on. Between classes and committees and other such responsibilities, there is little freedom to set one’s own schedule.

I worry that this myriad of non-interesting-problem related responsibilities really prevent professors from working on interesting problems. I notice this particularly when I am the only one making progress on my advisor’s research projects.

I understand that there is more to doing research than sitting down and solving a new and interesting problem. I do like teaching, attending talks, meeting with other researchers, and reading papers, and I appreciate these other tasks that just must get done. But I am concerned that the majority of a professor’s time is spent on not-research, and that there seem to be weeks and months at a time that professors do not sit down and solve a problem—unless they deal with uninteresting things all day and start doing research at 11pm¹.

I do not want to work until 11pm every day, because there are other things in my life that I like doing.

I am not even sure professors get to choose their own research agenda. This seems particularly true of tenure track positions. To get tenure, you seem to require lots of publications at highly rated venues. This does not encourage doing good work. It encourages doing popular, easy work; it encourages slicing good work as thinly as possible; it encourages padding papers with co-authors so they will pad their papers with you as a co-author; it encourages ignoring your students and your teaching; it encourages working too much to be healthy. If you do not get tenured, even if you do a good job, you are fired.

In general, incentives seem setup totally wrong. For instance, professors seem to need Ph.D. students to get any work done, possibly caused by the hundreds of other things they have to do. But this incentives them to hire more Ph.D. students, regardless of whether or not the market needs more Ph.D. students. Given how competitive the academic job market is, and how narrow the skill set a Ph.D. provides, I am not convinced the market needs any more Ph.D.s. As a final example, professors with tenure are not encouraged to do a good job at literally anything.

Instead, the incentives in academia should encourage solving novel, interesting, hard problems, but not punish you for getting there late or taking a long time. They should encourage collaboration, and not discourage discussing early work for fear of getting scooped. They should encourage doing good work continuously, and not lots of good work for 6 years followed by no incentives. They should encourage a healthy work/life balance.

At least in industry there is one clear motive: profit. If you can convince someone (with enough decision making power) that your interesting problem increases profits—brings in revenue, brings up productivity, brings down cost—you can do it. Maybe you can’t set your own schedule as easily, but that is changing. More and more companies allow flexible hours and telecommuting. There is a standard on how much your work: 40 hours a week. And you make double what you make in academia.

¹ Personal communication about a senior researcher.

TLDR: Follow me on Twitter if you want to see me share stuff.

For the last n months, I have been using IFTTT to mirror my Twitter account to my Facebook account. I am going to stop doing this because neither Facebook nor IFTTT support what I need to make this sensible.

I started using IFTTT because, while I maintain a Facebook account and connect with several people exclusively through Facebook, I primarily use Twitter. Twitter is easier to use for me, partly because posts are shorter and I manage my time carefully, and partly because bitlbee gives me an interface that matches my natural environment. Unfortunately, Facebook is not great at the same sorts of things that Twitter is.

Twitter automagically supports links and pictures that you tweet, linking and embedding them as appropriate depending on your client. Twitter supports a much more active stream of thoughts. Twitter makes it absurdly easily to share other peoples’ thoughts with attribution, i.e., retweets. Twitter has course-grained privacy, and the usual workflow for having private and non-private tweets is via multiple accounts, which Twitter clients support.

On the other hand, Facebook requires you to explicitly tell it what to do. If you post a link, but do not claim it is a link, Facebook will merely hyperlink the URL rather than embed the link. Facebook supports longer posts but fewer of them. Facebook seems to encourage sharing your own thoughts. Although it does support sharing, it is not nearly as simple, and is easy to remove to original attribution (presumable for privacy of the original author). Facebook supports fine-grained privacy of individual posts, but this too requires more interaction, i.e., explicitly telling Facebook what to do.

I setup IFTTT to simply mirror my tweets to Facebook, sharing them only with friends. However, I want some tweets to be public, and some to be friend-only. I want links and pictures to be automagically embedded. I want my tweets to appear without attribution, and retweets to appear with attribution. I only want some tweets to be mirrored.

While IFTTT has some support for some of this, for instance, using hashtags to denote which tweets should be thought of as links and the link embedded, it does not support everything that I want. Part of this is on Facebook for not being automagical, but I think this is probably a feature for Facebook since too much automagic is not appealing to many users. I, however, like automagic.

So, I am turning off IFTTT, and my Facebook posts will all but disappear. If you care about my random day-to-day thoughts, follow me on Twitter instead. All my Facebook messages go to bitlbee though, so I am still accessible through that.

A couple weeks ago, I wrote that I was beginning to hate conference talks. The next morning, I woke up with 50+ Twitter notifications caused by people debating that point. I have reconsidered my views.

In my earlier post, I point out that the typical advice I hear is “The talk should be an ad for the paper”. After several discussions, I think this is bad advice. Instead, Lindsey Kuper and Chris Martens encouraged me to ignore this advice and instead make my talk a performance.

At first, I was unsure what this meant. In fact, I am still not quite what this means. What does it mean to perform a paper? But I followed it anyway.

Essentially I tried to communicate, at a high-level, why I think this work is cool, and what parts of the work are most interesting. I tried to tell a story about what inspired this work, why I care about it, and what came out of it. I did not try to show many technical details; I showed only those necessary to tell the story of this work. I did not try to explain the particulars of all this work; I showed only those necessary to fit the work into the context of the story I wanted to tell.

I think the end result is actually an effective ad for the paper. However, by approaching the talk differently, I produced a much better talk (IMHO). And thankfully, I am not alone in that opinion. For example, I was very excited after my initial practice talk when Matthias called the talk “90% perfect”, in defiance of a NU PRL tradition of not dwelling on positive aspects and only giving constructive criticism after a practice talk.

A video of this talk is online here.

I am beginning to hate conference talks. I am in the midst of writing a conference talk for my recently accepted paper. Although I have only given one conference talk thus far, I have attended several conference and listened to many talks. These experiences have convinced me that conference talks are largely pointless.

I do not find conferences to be pointless. The papers are usually well written, if dense. The conferences themselves always lead to interesting conversations with clever people. I always return from a conference filled with creative energy. And, I admit, I like the excuse to travel to interesting locales.

However, the talks themselves are pointless. Most talks I have attended are terrible. Those that are not terrible I do not remember much of anyway, except that I should go read that paper. Of those talks, I would have made the same decision after reading the abstract for the paper. The talks add nothing because the talk slots are too short to communicate any technical material.

It is not entirely the fault of the speakers. For one, there is little incentive to give a good talk. If you give a good talk, then maybe you convince someone to read your paper, and maybe people remember who you are. This might be important if you are on the job market, but it does not matter for everyone else. Besides, most people will forget the talk in a month, good or bad.

Even if you are a perfectionist so incentive does not matter, it is not easy to craft a good talk. Conference papers are often complex and dense pieces of work. Frequently, the papers omit many details due to space, so completely understanding the work requires not only the paper but a technical appendix or code artifact published separately. Authors (usually (maybe only sometimes)) spend a great deal of time polishing these papers and supplementary materials to effectively communicate a complex and dense piece of work. The slot for the conference talk is 15—20 minutes, in which a speaker much fit a 12-page paper plus supplementary material?

“No! Obviously as a speaker you must not do that. The talk should be an advertisement for the paper. It should be an overview of the paper. It should communicate the key technical ideas and convince people to read the paper.”

What silly advice. I hate advertisements. Why should I sit through sessions and sessions of advertisements?

“No! Obviously as an audience member you must not do that. Just go read the abstracts and find the talks you want to attend. Skip the rest to have conversations with colleagues and authors.”

Okay, so the audience is going to read the abstract to convince them to see a talk that convinces them to read the paper of which they just read the to convince them to see the talk that convinces them to read the paper? This is circular reasoning that wastes the time of both the speaker and the audience.

As a speaker and writer, I have already spent a lot of time and effort on the paper. I have crafted the abstract and introduction to communicate the key technical ideas and give an overview of the paper as precisely and concisely as possible. Shortly thereafter, I have carefully written the rest of the paper to effectively communicate the technical contributions in as much detail yet as concisely as page limits allow. Besides, I had to write them anyway to effectively communicate my research. Why should I reproduce these efforts in a short talk that must communicate less due to the nature of the talk and the audience?

As an audience member, if I want an overview of the paper, the abstract and introduction section provide this. The author already spent a great deal of time writing these sections, which communicate more thoughts in less time than the talk will. If I want more details, these sections are conveniently located with the rest of the paper. Besides, I need to read the abstract anyway to figure out which talks to attend and which papers to read. Why should I then sit through a talk that advertises a paper that I have already decided whether or not to read?

“Well the talks give an excuse and talking points around which we can organize a conference.”

Well why can’t we find a better excuse or better talking points? Why not give longer highly-technical talks that supplement the paper, or questions-and-answer style talks for those who have read the paper and want more? Or why not make the papers more open ended so talks can be more speculative?

I do not know what should go in place of the current conference talks, but the current system seems utterly pointless and results in completely wasted effort.

A while back I wrote a post about paranoia in which I was considering allowing Google or Apple to manage things like my calendar and contacts. Since then, I have reequipped my paranoia hat. This week I setup my own WebDAV, CalDAV, and CardDAV servers and secured them behind an nginx proxy which provides SSL encryption and HTTP authentication.