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!

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.

• 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 fast as a true JIT. Self-built versions also support JIT, using modern self-JIT techniques and tunneling approaches.
• Dialect: A scheme-based swiss army knife for wrist-worn computation, designed to work fully independently of your iPhone and provide real-world capability and power. It is built around a custom editing experience that only a Lisp could easily bring.
• Symbat: Integrating Numbat into Obsidian with an eye toward becoming a notes-integrated computer algebra system.
• Fluidity: Better handling for link completions and aliases in Obsidian.
• 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.
• Recursion Music: Mixing and mastering in a custom-built studio.