Inside 206-105

Existential Pontification and Generalized Abstract Digressions

Computer Science

Calculating Shanten in Mahjong

Move aside, poker! While the probabilities of various poker hands are well understood and tabulated, the Chinese game of chance Mahjong [1] enjoys a far more intricate structure of expected values and probabilities. [2] This is largely due in part to the much larger variety of tiles available (136 tiles, as opposed to the standard […]

HotOS “Unconference” report:
Verifying Systems

Ariel Rabkin has some code he'd like to verify, and at this year’s HotOS he appealed to participants of one “unconference” (informal breakout sessions to discuss various topics) to help him figure out what was really going on as far as formal verification went. He had three questions: "What can we verify? What is impossible […]

NLP: the missing framework

So you want to make a web app. In today’s world, there is a panoply of software to assist you: you can use an all-in-one framework, or you can grab libraries to deal with the common needs of templating, database access, interactivity, etc. These libraries unify common functionality and take care of edge-cases you might […]

Functional Encryption

Joe Zimmerman recently shared with me a cool new way of thinking about various encryption schemes called functional encryption. It’s expounded upon in more depth in a very accessible recent paper by Dan Boneh et al.. I’ve reproduced the first paragraph of the abstract below: We initiate the formal study of functional encryption by giving […]

Extremist Programming

Functions are awesome. What if we made a PL that only had functions? Objects are awesome. What if we made a PL where everything was an object? Lazy evaluation is awesome. What if we made a PL where every data type was lazy? Extremist programming (no relation to extreme programming) is the act of taking […]

ACM XRDS: Jeff Dean profile

I was wandering through the Gates building when the latest issue of the ACM XRDS, a student written magazine, caught my eye. “Oh, didn’t I write an article for this issue?” Yes, I had! The online version is here, though I hear it’s behind a paywall, so I’ve copypasted a draft version of the article […]

Visualizing satisfiability, validity & entailment

So you’re half bored to death working on your propositional logic problem set (after all, you know what AND and OR are, being a computer scientist), and suddenly the problem set gives you a real stinker of a question: Is it true that Γ ⊢ A implies that Γ ⊢ ¬A is false? and you […]

GET /browser.exe

Jon Howell dreams of a new Internet. In this new Internet, cross-browser compatibility checking is a distant memory and new features can be unilaterally be added to browsers without having to convince the world to upgrade first. The idea which makes this Internet possible is so crazy, it just might work. What if a web […]

“This is really the End.”

Done. This adjective rarely describes any sort of software project—there are always more bugs to fix, more features to add. But on September 20th, early one afternoon in France, Georges Gonthier did just that: he slotted in the last component of a six year project, with the laconic commit message, "This is really the End." […]

Why verification results in higher quality code

Correctness is overrated. After all, no one knows what it means for any reasonably complicated system to be "correct", and even when we do, the mileposts move around on a daily basis. With the raison d'être of formal verification stripped away, can we still consider it a worthy goal? Perhaps verification results in higher quality […]