I found my current niche in software back in college. One homework assignment in a required intro course was to write an AI to play Pokemon. It was a functional programming course taught in a language called Standard ML. After everyone submitted the homework, the course would run a tournament between everyone’s AIs. It was intended as a fun, open-ended way for students to apply functional programming to a game they already know and love.
The problem was, I happen to have never played Pokemon.
Rather than learning how Pokemon is played, for some reason I thought it would be easier to write a neural network to learn Pokemon for me.
After spending too long implementing a neural network with feedforward, backprop, and gradient descent, I still had to train it. The course had set up a server we could use to play our AIs against those of other students, but I quickly found there weren’t enough active players for me to get enough data to train on. I came up with a hacky way to train the network (years later I have learned the technique I used is called “self-play reinforcement learning”). After using a late day to get an extra 24 hours to train on the most powerful processor I could find in EC2, I submitted my code. My AI lost every game it played and was eliminated from the tournament immediately.
I entered college thinking I wanted to specialize in machine learning, but when I got around to taking my first machine learning class, somehow it made me dislike calculus. At around the same time, I took the aforementioned functional programming course. One takeaway from my brief and unsuccessful foray into machine learning in Standard ML was how much fun I had hacking on functional code in a language with such a great type system. I TA’d the functional programming course the following semester, and over the next few years I went on to take every course in logic and programming language theory that my school offered. I also did research on programming language theory in my junior and senior years.
Type systems and logic (which are the same thing) interested me because of their potential to amplify what a programmer can do, and because of how underrated these fields are. It feels like there still remains so much space for providing value by bridging the gap between the world of formal logic and the world of software engineering.
After college I got involved in one such effort when I joined Flow, a static typechecker for JavaScript (like TypeScript) with an emphasis on soundness. I remember adding Flow to a JavaScript project that I had made years prior and getting to delete around half of the lines of code as the static typing made them no longer necessary.
With the rise in popularity of things like Flow, TypeScript, MyPy, OCaml, and Rust — as programming languages become more and more “ML-like” — it feels like the world is coming to appreciate how much programming work can be saved by type systems. Things continue to emerge and flourish in the comfortable space in between Haskell and Lisp.
I’m excited to have joined Oso because we’re building a new bridge between formal logic and software engineering. Just like how it took time since the advent of ML for its aesthetics to define the most popular languages, Oso is on the cusp of bringing the declarative power of things like Prolog to solve authorization in a way that saves people tons of time and effort. Thousands of developers already use our declarative programming language Polar to power their authorization logic and more, and we’re just getting started in this unique design space.
If developing a new programming language and solving for authorization sounds like something you’d be interested in, see our open roles.
