A year with OpenAI's Codex

Over the past year I have used Codex to try things I had wanted to do for a long time, and others that only occurred to me once trying became simple enough.

• A BitTorrent client in Haskell, reaching roughly 30 Gbit/s of download and upload payload throughput over loopback on one machine. This includes protocol processing but no physical network. It uses safe and unsafe C FFI calls, reusable buffers and allocation-free hot paths, with POSIX sockets, pthreads, OpenSSL’s libcrypto and SQLite. Removing allocations required explicit yields: GHC normally handles timed context switches at heap-block allocation, a scheduling safe point. With 64-byte-aligned buffers and tuned buffering, my OpenSSL-backed SHA-1 hashing also outperformed the sha1sum executable from GNU Coreutils on my machine. I was mainly motivated by disliking how current mainstream clients behave, none of them capable to track 1M torrents without using massive amounts of memory. I barely got Transmission to run on a Raspberry Pi Zero 2 W.
• A torrent tracker, reaching about 5 million scrape responses and 1 million announces per second locally through HTTP batching and pipelining. A bounded ring buffer tracked recent peers, seeders and leechers. The client’s SQLite-backed scheduling reached about 180,000 announces per second. I used tools such as SciPy to explore how quickly reannounce jitter smooths an initial burst into a steady request rate. My NIC could not handle the traffic needed to reach 5 million requests per second.
• Nadimak, a grammatical Croatian phrase generator I had always wanted to make. Its 6.5 MB compiled grammar has 248,619 construction plans and about 442 quadrillion combinations, or 1.77 quintillion with separator choices. A JavaScript implementation would take much less source code. The meanings can be strange. Add syllable counting and it could generate constrained poetry.
• Ansible infrastructure for a VPS, a Raspberry Pi Zero 2 W and a Raspberry Pi 5. More than 10,000 lines of strictly typed Python monitor disk errors, service failures and host metrics through Sentry. I run Forgejo, an Anki sync server and other services, with monitored restic backups everywhere. They work extremely well. I would never have attempted this much infrastructure before. Maintaining it at work is enough of a job already. 😅
• adjust, a local document-search harness using SQLite FTS5 and brute-force reading by small Gemma 3 and 4 models. Batching through vLLM reached thousands of tokens per second in aggregate on my RTX 3090. It works well on my thousands of EPUB books. An interesting code-generation experiment, though I realized I wasn’t interested in the answers my collection could provide.
• Formalizing inductive proofs in Lean in fixed-rtrt. Donaghey’s squeeze [Dona80] and the result in Shapiro’s The Cycle of Six [Shap79] were easy to formalize. The full classification problem is still open.
• Exploring reflections and bijections between Catalan objects by implementing Viennot’s jeu de taquin [Vien18], the Loday–Ronco product [LoRo98] and the Aval–Viennot sharp product [AvVi09]. A recurrence as simple as \(A_{n+1} = RT(A_n) + \ell\) led me to powers of two and h-Stöhr sequences in related return-time problems.¹ Transform the object, append a leaf, repeat. In a related model, iterating Kreweras complement and inserting a singleton gives 1, 2, 4, 7, 10, ... as the steps where the permutation fixes 1. A larger construction using Armstrong’s multichain framework [Arms07] realizes every \(h\)-Stöhr sequence, \(h\ge2\), as the steps where a selected product of its factors fixes 1. A growth rule as simple as \(A_{n+1}=K(A_n)+\ell\) gives very different return patterns depending on \(K\), from symmetry that seems to disappear to periodic behavior with an exact description.

• A subtitle harness using Gemma to extract text from sparsely sampled movie frames, and vLLM to translate and revise existing subtitles into SRT files.
• Turning public-domain book scans into typeset LaTeX, with PDF and EPUB output. Thirty minutes for something I would never have attempted. Recording the typesetting patterns in AGENTS.md brought the second book down to five minutes.
• A music app that imports the metadata of my 35 GB library in under a second, with fast virtualized scrolling and strictly typed Rust and TypeScript. The iOS playback widget was extremely buggy and tricky to get right. Adding a volume meter made playback glitch badly. Even gapless playback was a struggle, something foobar2000 managed decades ago. 😂
• A powerlifting app that takes few taps to use, with Bluetooth Low Energy heart-rate tracking. I’ve used it daily for months. Easy to make reports to my coach. Both apps have personal interfaces over reusable backends. They made me realize foobar was way ahead of its time. Today, all apps should be like foobar.

Simpler attempts:

• Exploring monotiles in single-page HTML/CSS/JS apps to design a tiling for part of a shirt. How nice will it look while windsurfing on the coasts of Bonaire?

  

  

  

  

• Rewriting old scripts such as cmus-status-scrobbler with strict types and explicit data structures, making them easier to change.
• A strictly typed, concurrent music conversion script with a curses terminal interface. Parallel FFmpeg jobs convert my FLAC library to AAC, Opus or MP3, skipping existing conversions.
• Generating Anki cards for lyrics, poems and the screaming styles I hear in Deafheaven. I use LRCLIB’s lyric timings to cut audio snippets for recognition and continuation cards. It’s fun to let the brain learn through quick associations. It helped me immerse myself in a brilliant Deafheaven performance in Nijmegen, Netherlands.
• Investigating variants in my own genetic data locally.
• Studying CPython: changes to cyclic garbage collection, reference ownership, thread synchronization, and dictionary, list and set implementations. Also Python 3.11’s lighter interpreter frames and inlined Python calls: ordinary Python-to-Python calls no longer need a recursive C evaluator call, and Python frame objects are materialized only when needed.
• Tampermonkey scripts to put buttons where they should be, add 2.5×, 3× and 100× playback controls for YouTube and <audio> elements, and make many other small fixes.

I learn a lot from finding and fixing quirks in these projects. Most of the work is in getting the details of behavior right. Apart from separating external calls from core logic, abstractions and OOP patterns haven’t made that work much easier for me.

I want to try Verus for Rust and see how much specification and proof code it takes, and how verification changes the design. I expect the code to move toward explicit state machines, with each state carrying the data it needs. Encapsulation alone leaves that state implicit in combinations of flags, optional fields and other variables. I want the current state and its allowed transitions to be explicit, making invalid combinations harder to represent and error recovery easier to reason about and prove correct.

There are many ideas that build on things I already have, or explore other parts of my interests. Time is limited. I would have left most of these unattempted, and now I get to find out where they land.

Bibliography