I'm building OATP, based on my earlier Haskell project, online-atps. Written in Lean 4, OATP has a REPL and CLI for interacting with automated theorem provers. It parses TPTP, runs local and online provers, and provides reproducible artifacts, diagnostics, and more.

Before I could build OATP, I had to develop some tooling. You might find it useful too.

Grip is an efficient, graded, byte-oriented parser-combinator library inspired by my friend's project, prim-parser. The grade tracks input consumption, allowing recursive parsers to be structurally terminating rather than marked partial.

Using Grip, I can parse TPTP in grip-tptp, and JSON in grip-json. Another thing I wanted for Grip is better error messages, so that's grip-diagnostics, easy to read parse errors.

CLI? optparse-applicative? in Haskell? I build Argus to handle typed command-line parsing. Flag values are Grip grammars, and both the help text and shell completions come from one inspectable spec. OATP uses it.

For ANSI colours and styled text, I built termcolor, with layout (Unicode width, wrapping, boxes), diagnostics (caret spans, gutters), widgets (pure progress bars and spinners), terminal and repl, where only the last two touch a real terminal, so pure consumers never link IO.

calc-chat is a demo of the termcolor stack: a chat-shaped terminal calculator.

precommit-lean has shared hooks for Lean style and module names, and an axiom audit that limits the accepted axioms to propext, Classical.choice and Quot.sound. Quite opinionated. It also carries the /lean-format command I run on every declaration. It only changes whitespace and compares token streams to check that.

I used to think Haskell would become the next big language for me at least. Now I think it is any theorem prover with general-purpose programming support and dependent types. That is Lean 4, it could have been Agda, but AI simply pushed Lean so much, made it mainstream, that it would be a mistake to not learn it, and it's really fun, actually! I still miss Agda-way of proving things, proof-term construction I mean.

On compilers, at Heliax, I was one of the main contributors to the FP Juvix programming language and the maintainer of juvix-docs, vscode-juvix, juvix-stdlib and juvix-mode, plus more that never got a repo. I also created juvix-mkdocs for literate documentation. It is used for the Juvix FP tutorial.

I also worked on distributed systems there. Main conclusion, distributed systems are hard, theoretically and practically. I learn and now fan of the actor model and the clarity of its variations. I explored and formalised one in mailbox-actors, where mailboxes are promoted to first-class actors, and the same idea specifies node protocols as engines, documented with a ticker as an example. Another cool idea in the literature is Tango, I did a limited version of it in elixir-tango, replicated in-memory data structures. I also experimented with formal specifications of a distributed virtual Machine in AVM Lab, from its instruction set and interpreter semantics to interaction trees and sequential objects. Interactions trees are quite nice! big fan of this simple but powerful construction.

Back in day, during my master's, I wrote online-atps to run the provers from SystemOnTPTP. I also contributed to apia, which discharges Agda first-order goals with them. athena turns the Metis proofs that come back into checkable Agda terms. It emits into agda-prop and agda-metis, classical propositional logic and Metis proof reconstruction in Agda, with prop-pack as the problem set.

During my PhD, I worked on synthetic graph theory, graph constructions formalised in HoTT. I co-created agda-unimath, a formalization of univalent mathematics, though I have been mostly absent from it since. If HoTT is your thing and you're learning it, check out my hott-cheatsheets and mini-hott.

I also wrote agda-pkg, the apkg package manager for Agda, years ago. It has been unmaintained for nearly as long. I don't think Agda needs a package manager anymore.

Before all this, I wrote a lot of Python. flask-ponywhoosh provides full-text search for Flask on top of ponywhoosh.

Nowadays, I build with agentic tools at work and have more recently started using them for my personal projects. A lot of people are against it for several reasons. To me, AI is another tool in my toolbox. I continue building as before, but more, and it is hard to keep the same level of supervision. For the projects I really need, I still write and review every line. But I don't want to spend all my time and energy reviewing everything I try. Some of these projects were built with AI, some only in part, some on my own, and some before any of this. The level of supervision varies. That distinction stopped mattering to me.