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.

I’m converting my blog and website to Frog/Scribble.

This is my first post.

I like it better than Octopress. I get Racket and Scribble for templating, Markdown or Scribble support for blogging and pages, and I don’t need Ruby. The conversion process was dead simple, given that Octopress posts were already in Markdown.

FASTR is a bill to ensure all publically funded research is open access. I urge you all to contact your congresspeople and demand they support this bill.

I finally switched my blog from WordPress. Despite my aversion to ruby, I went with Octopress. It’s a little easier to work with and has a slightly nicer default infrastructure.

I have a Windows partition on my machine, because sometimes there are things wine can’t handle, and sometimes I need more performance than VirtualBox can handle.

So recently I’ve been getting all my games to run under linux. As part of this process, I’m learning all about my ATI drivers, because graphics drivers are universally terrible. However, under linux, you can tinker more freely to make them (slightly) less terrible.