Earlier this year, Woodie Flowers wrote this criticism of MITx:
We seem to have decided to offer “courses” rather than participate in the exciting new process of replacing textbooks with more effective training tools.
Logitext, true to its name, was intended to explore what a chapter from a next-generation textbook on formal logic might look like. But if you asked anyone what subjects the most important textbooks of this century would be about, I doubt logic would be particularly high on anyone’s list. In terms of relevance, Logitext misses the mark. But I do think there are some design principles that Logitext helps elucidate.
Read more...
You can view it here: An Interactive Tutorial of the Sequent Calculus. This is the “system in three languages” that I was referring to in this blog post. You can also use the system in a more open ended fashion from this page. Here’s the blurb:
This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic.
Read more...
It is once again time for Ubuntu upgrades. I upgraded from Ubuntu Oneiric Ocelot to Ubuntu Precise Pangolin (12.04), which is an LTS release. Very few things broke (hooray!)
- The Monospace font changed to something new, with very wide glyph size. The old font was DejaVuSansMono, which I switched back to.
- Xournal stopped compiling; somehow the linker behavior changed and you need to specify the linker flags manually.
- gnome-keyring isn’t properly starting up for us non-Unity folks. The underlying problem appears to be packaging errors by Gnome, but adding
eval `gnome-keyring-daemon -s to my .xsession` cleared things up. - The battery icon went away! I assume some daemon is failing to get run, but since I have a very nice xmobar display I’m not mourning its loss.
- Default GHC is GHC 7.4.1! Time to rebuild; no Haskell Platform yet. (Note that GHC 7.4.1 doesn’t support the gold linker; this is the
chunk-size error.)
I also upgraded my desktop from the previous LTS Lucid Lynx.
Read more...
“…so that’s what we’re going to build!”
“Cool! What language are you going to write it in?”
“Well, we were thinking we were going to need three programming languages…”
“…three?”
“…and they’ll be research programming languages too…”
“Are you out of your mind?”
This was the conversation in streaming through my head when I decided that I would be writing my latest software project in Coq, Haskell and Ur/Web. I had reasonably good reasons for the choice: I wanted Coq because I didn’t actually want to implement a theorem prover from scratch, I wanted Ur/Web because I didn’t actually want to hand write JavaScript to get an AJAX interface, and I wanted Haskell because I didn’t want to write a bucket of C to get Ur/Web and Coq to talk to each other. But taken altogether the whole thing seemed a bit ludicrous, like an unholy fusion of a trinity of research programming languages.
Read more...
While working on my senior thesis, I had to write a prior work section, which ended up being a minisurvey for the particular subfield my topic was in. In the process, a little bird told me some things…
- If you can, ask someone who might know a little bit about the subject to give you the rundown: there’s a lot of knowledge in people’s heads which never got written down. But also be aware that they will probably have their blind spots.
- It is better to do the literature review later rather than earlier, after you have started digging into the topic. I have been told if you read the literature too early, you will get spoiled and stop thinking novel thoughts. But I also think there is also a little bit of “you’ll understand the literature better” if you’ve already thought about the topic on your own. Plus, it’s easy to think that everything has been done before: it’s simply not true! (But if you think this, you will get needlessly discouraged.)
- Don’t indiscriminately add papers to your database. You should have something you want to do with it: is it an important paper that you have to cite because everyone knows about it? Is it directly addressing the issue you’re dealing with? Does it happen to be particularly well written? Is it something that you could see yourself reading more carefully later? Don’t be afraid to toss the paper out; if it actually was important, you’ll run into it again later.
- Every researcher is a historian. When you look at a paper, you’re not just looking at what is written inside it, but its social context. There’s a reason why “prior work” is so important to academics. If you don’t understand a paper’s context, it’s unlikely you’ll understand the paper.
- Researchers don’t necessarily talk to each other. Pay attention to who they cite; it says a little bit about what community they’re in.
- Researchers are happy to send you copies of papers they have written (so fear not the paywall that your university hasn’t subscribed to). They may even volunteer extra information which may come in handy.
- Be methodical. You’re doing a search, and this means carefully noting down which papers you skimmed, and what you got out of them, and keeping track of other veins of research that you need to follow up on. It’s like chasing a rabbit down a hole, but if you have some clearly defined search criteria, eventually you’ll bottom out. You can prune the uninteresting papers later; the point here is to avoid duplicating work.
- Read papers critically. Not everything that is published is good; that’s the point of research!
What are your favorite maxims to keep in mind while you’re surveying the literature?
Read more...
Ur is a programming language, which among other things, has a rather interesting record system. Record systems are a topic of rather intense debate in the Haskell community, and I noticed that someone had remarked “[Ur/Web has a http://www.impredicative.com/ur/tutorial/tlc.html very advanced records system]. If someone could look at the UR implementation paper and attempt to distill a records explanation to a Haskell point of view that would be very helpful!” This post attempts to perform that distillation, based off my experiences interacting with the Ur record system and one of its primary reasons for existence: metaprogramming. (Minor nomenclature note: Ur is the base language, while Ur/Web is a specialization of the base language for web programming, that also happens to actually have a compiler. For the sake of technical precision, I will refer to the language as Ur throughout this article.)
Read more...
This is a very quick and easy fix that has made latency on Ubuntu servers I maintain go from three to four seconds to instantaneous. If you’ve noticed that you have high latency on ssh or scp (or even other software like remctl), and you have control over your server, try this on the server: aptitude remove libnss-mdns. It turns out that multicast DNS on Ubuntu has a longstanding bug on Ubuntu where they didn’t correctly tune the timeouts, which results in extremely bad performance on reverse DNS lookups when an IP has no name.
Read more...
If you haven’t noticed, these are coming in the order of the visit days.
Whereas the weather at UPenn was nice and sunny, the NJ Transit dinghy rolled into a very misty Princeton. Fortunately, I had properly registered for this visit day, so the hotel was in order. I was a bit early, so I met up with an old friend who had recently penned this short story and we talked about various bits and bobs (“I hear you’re up for a Hugo!”) before I meandered over to the computer science building.
Read more...
Note: this is not a discussion of Hilbert’s formalism versus Brouwer’s intuitionism; I’m using formalism and intuition in a more loose sense, where formalism represents symbols and formal systems which we use to rigorously define arguments (though not logic: a sliding scale of rigor is allowed here), while intuition represents a hand-wavy argument, the mental model mathematicians actually carry in their head.
Formalism and intuition should be taught together.
Read more...
