👋 I'm Ara

I'm Ara Adkins, a compiler and runtime developer, and type-theorist with a passion for formal verification. I love to work on UX, performance, and enabling better and safer software through type systems and verification. I also work on cryptographic systems and machine learning from time to time, and have a passion for computer graphics and simulation.

In my spare time, I run an audio engineering business doing mixing and mastering in the music industry. I also love to make things of all kinds, and to ski, sail, and practice parkour and martial arts. I also like to go trail wheeling in my car!

💻 Projects

Listed below are a few of the major projects that I am or have been involved with that I'm proud of. The public ones are linked.

• Lampe: Formalising the semantics of Noir in Lean so we can reason about the correctness of Noir programs with a focus on UX and usability for non-professionals trying their hand at verification.
• tctiSH: An iSH-alike that runs under the TCTI pseudo-JIT to run arbitrary Linux software on an iOS or iPadOS device using user-mode emulation. The threaded interpreter boasts improved performance over a standard interpreter, but is not as good as a true JIT.
• Lagrange: A dependently-typed programming language with dependent, polymorphic row types used to give it the flexibility of dynamically-typed systems.
• REPLive: A Swiss Army Knife of computation for your pocket or your wrist. This project aims to make computing on the go as easy and intuitive as it can be.
• Recursion Music: Mixing and mastering in a custom-built studio.