In this post I precisely define common compiler correctness properties. Compilers correctness properties are often referred to by vague terms such as “correctness”, “compositional correctness”, “separate compilation”, “secure compilation”, and others. I make these definitions precise and discuss the key differences. I give examples of research papers and projects that develop compilers that satisfy each of these properties.
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
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.
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.
This post is not going to tell you how to be more productive.
It seems like every person on the internet has The One True Way to achieve maximum productivity. Before I tell you why I think they’re full of shit, let me confess something.
I don't want to be super productive.
Productivity is the wrong thing to optimize.
If you need some advice, either you have a specific problem and should seek a specific solution, or you’re procrastinating.
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.
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.
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 recently1, 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 11pm1.
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.
1 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.
In my initial practice talk, the renowned critic Matthias called the talk “90% perfect”. He went on; I took numerous quotes:
- “I could get up and give this talk after seeing it”
- “I hate this work, I couldn’t care less, but I could give this talk, so well done, so perfect for the audience”
- “Proof is exemplary high-level, intuition-based proof”
- “QED was perfect. And QED (ish) was even better.”
Of course, he went on to dismiss the audience as a bunch of theoreticians, and said that the talk was perfect insofar as it perfectly explained utterly pointless work, but I assume he said this only so he could not be accused to giving praise.
A video of this talk is online here.