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.

My monthly cellphone bill averages less than $10 per month. I have a smartphone. I have data, texting, and voice, and I use them. Let me tell you how I achieve such a low bill.

Disclaimer: I will get a credit if you sign-up through my referral link, but so will you.

I need to write more.

In order to practice writing clearly and concisely,

to organize my thoughts,

to let small thoughts grow,

to store my thoughts in a less imperfect storage medium,

I need to write more.

And so begins a weekly¹ Rambling.

¹ hopefully.

Today I read Ur: Statically-Typed Metaprogramming with Type-level Record Computation. This paper presents the Ur language, a functional programming language based on an extension of System Fω. The novel idea is to use type-level functions as a form of type-safe meta-programming. The paper claims this novel idea enables safe heterogeneous and homogeneous meta-programming in Ur.

The interesting insight is that type-level computation may be valuable outside of dependently typed languages. The paper quickly and easily makes this case. The type-level computations reduce type annotations by enabling the programmer to compute types rather than manually write them everywhere. This could be a useful form of meta-programming in any typed language.

The claims about heterogeneous and homogeneous meta-programming seem overstated. Ignoring the novel ability to compute type annotations, type-safe heterogeneous programming could be as easily accomplished in any other type-safe language. I could just as easily (or more easily) write a program in Coq, ML, Haskell, or Typed Racket that generates HTML and SQL queries as I could in Ur. As for homogeneous meta-programming, restricting the meta-programs to record computations at the type-level seems to severely restricts the ability to generate code at compile-time and abstract over syntax, features which are provided by general-purpose meta-programming systems such as Racket’s macros or Template Haskell.

Yogurt is stupid expensive compared to the milk from which it is made, particularly if you want Greek-style yogurt.

So I decided to do it myself.

This summer I was in Paris for two months. Every day I got a fresh baguette for under €1. When I got back, I couldn’t eat store bought bread. It was terrible. And it cost $3. There’s no bakeries nearby, and the grocery store baguettes are crap and even more expensive.

So I decided to do it myself.

In my recent work, I found it useful to pair a term and its context in order to more easily reason about weakening the context. At the prompting of a colleague, I’ve been reading about Beluga, [1] [2], and their support for programming with explicit contexts. The idea seems neat, but I’m not quite sure I understand the motivations or implications.

So it seems Beluga has support for describing what a context contains (schemas), describing in which context a type/term is valid, and referring to the variables in a context by name without explicitly worrying about alpha-renaming. This technique supports reasoning about binders with HOAS in more settings, such as in the presence of open data and dependent types. Since HOAS simplifies reasoning about binders by taking advantage of the underlying language’s implementation of substitutions, this can greatly simplify formalized meta-theory in the presence of advanced features which previously required formalizing binders using more complicated techniques like De Bruijn indices. By including weakening, meta-variables, and parameter variables, Beluga enables meta-theory proofs involving binders to be much more natural, i.e., closer to pen-and-paper proofs.

Obviously this is great for formalized meta-theory. While I have seen how HOAS can simplify life for the meta-theorist, and seen how it fails, I don’t fully understand the strengths and weakness of this work, or how it compares to techniques such as the locally nameless. I’m also not sure if there is more to this work than a better way to handle formalization of binding (which is a fine, useful accomplishment by itself).

If anyone can elaborate on or correct my understanding, please do.

Sometimes I play minecraft. Sometimes I play a lot of minecraft and sometimes I just stop playing for months. Lately when I do play, I’ve bene playing with a slightly modified version of Tekkit and running my own server. I have a VPS that I probably under use, so I decided to run the server there for when I do play with my friends.

My VPS is not very powerful, and running a Minecraft server when I stop playing for months is a huge waste of resources. I sought a way to automatically bring the server up when I wanted to play and shut it down when I wasn’t playing for a while.

I wear my tinfoil hat proudly. I block ads, and JavaScript, and tracking cookies. I use HTTPS everywhere, I encrypt all my hard drives, I used randomly generated passwords, and I would encrypt all my emails if anyone else bothered to use GPG. I even run my own mail server, and have been considering running my own CalDAV and CardDAV server ...

But lately, I’ve been thinking maybe I should allow some ads and tracking, and let Google or Apple manage some of my data.