My name is Anthony Hart. I’m a data scientist and professional programmer with an interest in the theory of programming and the foundations of mathematics.

History

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 an actual application. I have an interest in emulation (a while back I implemented a simple emulator in Mathematica) and implementing mathematics on computers. For a while, I had an obsession with computer algebra systems, and I implemented a basic one as one of my first programs. It was awful and the code is lost to time, now, but I still maintain an interest in the topic.

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. The green icon on top of my blog comes from a graphical programming language that unfortunately never came to fruition. It denotes the type

Π x : nat . id(nat, plus(x, zero) x)

Hopes for the Future

I hope to eventually get a stable job where I can apply modern functional programming and algebraic mathematics to machine learning or other interesting applications. And perhaps, one day, I can make the perfect fusion of mathematics and a programming language.