I’m a programmer with data science training and an interest in the theory of programming and the foundations of mathematics.I started programming in C++ when I was 12, since then I’ve gained experience in a multitude of languages from Python, to Haskell, to Prolog, and more. I tend to program in Mathematica when prototyping and Haskell when implementing applications. I also have extensive experience with Python, mostly through the lens of Data Science.I’ve also had an interest in the foundations of mathematics for over a decade. My interest began when I was 14. Through my self-study, I eventually found and made small contributions to the Metamath project. After that, I got experience with a wider variety of perspectives on the foundations of mathematics, about HoL from Isabelle, and about dependent type theory from Agda. Some of my repositories relate to formally verified mathematics through dependent type theory. Nowadays, I’m interested in extensional approaches to type theory along the lines of Cedille and the various PRLs.From that experience, I make a hobby out of creating programming languages with sophisticated type-systems, some of which are capable of acting as foundations for mathematics. The handful that I’ve finished are posted to GitHub, but I’m constantly working on some new idea.I'm currently working as a formal verification engineer operating mostly in the crypto domain.