About

If you came here to learn more about the site itself, then you probably want to take a look at the colophon. This page is an introduction to me (not my website). Though there’s a section here devoted to my academic interests, if you’re looking for information about my formal academic background and my thoughts on education, you should visit the academics page instead.

I spend most of my time working at the intersection of theoretical computer science and mathematics. I’m particularly fascinated by category theory (often referred to as “general abstract nonsense”—not to be confused with concrete nonsense) and the powerful structures it gives us to describe the universe. While category theory is often dismissed as meaningless garbage, I subscribe to the higher structures point of view (popularized as the POV in the nLab as a play on Wikipedia’s “neutral point of view”), which posits that categorical algebra and related subjects have profound applications in a wide variety of fields.

I’m a founding member of functor.systems, which investigates categorical structures in computation, along with Youwen, Warren, Arvind, and Nicholas. At MIT, I created the OpenCompute Laboratory (stylized OCλ) with Anthony to explore these themes in greater detail and apply categorical logic to the formal verification of low-level systems. I also have the great opportunity to work in the Zardini Lab on co-design, a branch of applied category theory that deals with problems involved in the design of complex heterogeneous systems. This is my primary research focus at the moment.

⁂

I’m fascinated by a wide variety of subjects that I see as tackling difficult and profound questions through logical and axiomatic examination. This typically involves a lot of math, but not always. Some topics in fields outside mathematics and computer science that I find inspiring:

• Analytical mechanics

  • Viktoria Keusch’s thesis on a categorical interpretation of classical mechanics is particularly fascinating

  • I’ve been meaning to read Physics from Symmetry for a while, but unfortunately haven’t had the time to devote to it yet

• Social choice theory and related themes in political economy

  • I was initially interested in social choice theory because of Prof. Holliday and Prof. Pacuit’s work on the Stable Voting algorithm

    • By the way, did you know Prof. Holliday’s colleague in Berkeley’s philosophy department John MacFarlane is the creator of Pandoc, probably the most popular Haskell application ever developed

  • There are (unsurprisingly) connections to category theory, though I’ve not looked too deeply into this yet

  • In a more unexpected direction, there’s a lot of work on topological approaches to social choice that I’m particularly fascinated by

  • The “related themes in political economy” part is a bit vague, but generally I’m most interested in theoretical models of democratic decision-making; this tends to involve a lot of game theory (see below)

• Game theory

  • The foundations of microeconomics and also an extremely applied field involving some very beautiful mathematics

  • I don’t have much to say about this yet, mainly because I’m still not very familiar with the subject

• Linguistics, especially semantics

  • I like learning languages, and linguistics truly makes you question everything you thought (or didn’t think) about the fundamental structure of language itself

  • I’ve been told there’s a lot of overlap between semantics and type theory, though I haven’t yet explored the connection myself

• Philosophy, especially modal logic and epistemology

  • Modal logic is a very analytical branch of philosophy that has a lot to do with specifying axioms in mathematics

  • As you might imagine, there’s a lot of category theory involved

    • There’s an entire book on the subject actually, recommended to me by Prof. Holliday

  • Lately I’ve also decided I should take a look at the following two texts, as they seem to be widely embraced by category theorists worldwide (see Spivak’s values statement and the canonical category of being):

    • The Tao Te Ching by Lao Tzu, an ancient Chinese text tackling questions in metaphysics and unraveling the fundamental laws of the universe

    • Georg Wilhelm Friedrich Hegel’s Doctrine of Being, the first part of the first volume of the larger Science of Logic, which deals with the natural foundations of logic and introduces the ideas of being and becoming

If you’re interested in any of these subjects, feel free to contact me; I’m always happy to discuss these topics with other people.

⁂

When I’m not involved in these intellectual distractions, I spend my time hacking on free and open source software. I have strong beliefs about software freedom—the idea that software should be distributed without restriction and be free to modify, inspect, study, and redistribute. I think that such a philosophy leads to software that’s developed in the public interest and a more open, accessible society for all. These views—and the definition of free software (free as in freedom—the “free” in “free speech”, not “free” as in “free beer”)—might seem strange if it’s your first time hearing about this. Stallman’s essays on the subject are a good introduction to why we should care about such things.

Every hacker has a tool that they wield best. Mine is Haskell, the language of thought. It’s a programming language designed by mathematicians, not computer “scientists” or engineers. As a result, it’s notoriously difficult to learn, but when used well, it’s surprisingly powerful.

As a Haskell user, I am obliged to tell you two things. The first is that I must demonstrate moral superiority by insisting you learn Haskell as well. Just keep in mind that you will spend most of your time writing whitepapers. Second, I must warn you that I despise Lisp users, and so does the rest of the Haskell community, owing to differences in our preference for static types, among other things.

Part of the great illusion perpetuated by today’s hackers is the idea that programming is inherently about translating instructions into a form that can be understood by a computer. This is coding (not the intellectual kind) and has nothing to do with hacking (or as laypeople refer to it, programming). Instead, the Curry–Howard–Lambek correspondence tells us that writing a program is equivalent to putting together a mathematical proof. This might sound strange at first, but what it’s really saying is that, in order for your program to be useful, you must mathematically prove that it has the desired properties. Thus, there really is no distinction at all between the most applied domains in computer science and the realm of abstract mathematics.

I use a custom NixOS derivative called functorOS that I maintain collectively with other Nix hackers at functor.systems. There’s a lot to say about that, so I’ll leave it to another page on how I do my computing.