I’m Brian McSwiggen, a software engineer and computer scientist. I like to build things, and I like to think about programming languages, formal verification, and proof theory. I'm also a person. Reach out if you want to talk!
Play the Nepali board game Bagh-Chal (aka Tigers and Goats) with a friend, or against yourself. Sign in to view and create games. Python Flask backend, Angular Typescript frontend with Material styling, hosted on GCP with Cloud Run and Firestore.
A personal library webapp for myself and friends. Catalogue your books, track who you've lent them to, and browse the books your friends own. Python Flask backend and Angular Typescript frontend. Runs on GCP with Cloud Run and Firestore.
If you'd like to join the library system, shoot me an email and I can make you an account.
My solutions for the 2024 Advent of Code challenge in Kotlin, collecting all 50 stars.
Web tool for adjusting the pose of faces in images, based on a paper by Ohad Fried, written with JavaScript and WebGL. John Morone and I spent a summer building this as a demo for SIGGRAPH '16. Our site received over 40,000 uploads, was briefly on the front page of Reddit, and featured in a few news articles.
Unfortunately, the site is no longer running, and the code is kept in a private repository that I don't control.
As a 20% project while at Google, I collaborated with Andres Erbsen on Fiat Crypto, an effort to provide formally-verified code for cryptographic algorithms (and contribute it back to key security software like BoringSSL). I focused on fundamental point operations on elliptic curves, specifically Curve25519.
An earlier 20% project, I collaborated with Andrew Ferraiuolo on Project Oak, a platform for running distributed systems whose behaviors can be externally verified (e.g. for sealed computing). My contributions were primarily non-interference proofs (in Coq) of the Oak runtime, i.e. showing that secret data cannot influence publicly-observable behavior.
My senior thesis at Princeton, under Andrew Appel, part of the DeepSpec project. My goal was to implement a B+ tree (in Gallina, Coq's built-in functional programming language), write an abstract specification, and prove the implementation correct relative to that specification. In retrospect, this may have been over-ambitious: I completed the implementation and specification, but could only partially prove correctness.
(The official title was "Tree Automata Refinements on Algebraic Data Types", but that's a bit of a mouthful.)
I wrote a type-checker for a custom variant of OCaml with a more powerful type system. The idea is to extend OCaml's existing Algebraic Data Types with a limited set of type refinements. For example, it could express "a binary tree with an even number of layers" as a data type -- and then verify that anything in the program with the type TreeEven is, in fact, a binary tree with an even number of layers.
I enjoy doing many things. Most of which I’m not particularly good at (but I try to remember: sucking at things is okay). None of which I get to spend as much time doing as I’d like.
I’m a rock climber and cyclist. I also run and do yoga. I enjoy hiking, camping, and skiing when I get the chance.
I’m an avid reader; you can check out my collection of books in my personal library. I dabble in pottery. I played flute for a season with the NYC Googler Orchestra.
I’ve learned and lost several spoken languages. I speak French and some Spanish; at various points I have also studied Irish Gaelic, Arabic, and Portuguese.