the arc of software bends towards understanding
Some notes collected from a close read of Conal Elliot's Compiling to Categories and The Simple Essence of Automatic Differentiation. A colleague of mine was trying to define a "tree structure" of tensors, with the hope of thereby generalizing the concept to also work with tensors that have "ragged dimensions." Let's take a look: Suppose […]
Subtyping is one of those concepts that seems to makes sense when you first learn it (“Sure, convertibles are a subtype of vehicles, because all convertibles are vehicles but not all vehicles are convertibles”) but can quickly become confusing when function types are thrown into the mix. For example, if a is a subtype of […]
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 […]
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 […]
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 […]
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 […]
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 […]
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 […]
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 […]
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 […]