Jonathan Woollett-Light

Experience

Education

Portfolio

I am an expert in Rust, I am experienced in C++, C and Python, and I am familiar with Zig, Ada, aarch64 asm, RISC-V asm, JavaScript and CSS3+HTML5.

My programming language: A verifying compiler for bare-metal RISC-V, written in Rust. You write a small Python-like language, and the compiler accepts your program only if it can prove (by symbolically executing the actual machine code across every hardware-thread interleaving and every admissible type assignment) that no assertion can fail and no memory access is ever out of bounds, even for intentionally racy, lock-free code. Its type inference is complete, or ‘infallible’: a variable left unspecified is accepted exactly when some typing makes the whole program verify, because inference and verification are the same search. The proof’s by-products then drive code generation: it infers the memory layout and performs dead-data elimination, deleting interior bytes of live data it proved are never touched at runtime and rewriting the address arithmetic to match. It verifies the instructions themselves rather than high-level source, shrinking the trusted base to a small layout-only lowering plus the assembler and linker; conceptually it generalises Zig’s concrete compile-time evaluation to full symbolic exploration and turns Rust’s conservative data-race prohibition into exact, per-assertion race verification, with parallel and distributed (MPI) verifiers checked against a trusted single-threaded oracle. (source)

CV website: A simple website serving the latest version of my curriculum vitae. Written in LaTeX and rendered to a single self-contained page: a near-perfect Google Lighthouse score, light and dark mode support, less than 100kb in size, and neatly prints to PDF.

Hearts of Iorn 4 modding: I’m the owner and contributor to multiple Hearts of Iron 4 mods on the Steam Workshop (OWB – The Think Tank and Millennium Dawn: A Modern Day Mod). Working with mods and the often non-technical people making them requires a uniquely scrappy approach to development and a lack of hangups on formal processes (being able to work within what might politely be described as a mess), certainly a mindset shift from my traditional systems development.

Dating app: A dating app that learns user specific traits and preferences to match pairs. The server functions as an efficient monolith capable of handling all requests on a single Rust Axum server with in-memory stores and a local SQL store, achieving near 100% system utilisation capable of handling millions of users; supporting all the functionality of a typical tinder-like dating app.

CI Metrics: A website to track performance metrics (continuous benchmarking) and integrate with GitHub. A Rust Axum backend with a MongoDB database. Development focussed on experimentation with algorithms for anomaly detection to produce a solution that accomplishes what AWS Lookout for Metrics does, but at a much lower cost and complexity. This was motivated by my experience working on Firecracker at AWS where regressions that could have cost millions in production were almost missed, and certainly some were.

Live migration web server: A Rust server framework where a new server process can succeed a local old process in milliseconds with shared memory (or remotely in seconds over TCP) without dropping client streams. This can be used as a database server with in-memory data storage akin to Redis where queries are compiled as new functions.

RUST-AD: Auto-differentiation library with code transformation for both forward and reverse auto-diff written in Rust.

Mathematics Site: A mathematics website for automated marking. Built with a Rust Actix backend using a PyTorch semantic segmentation model, deployed with AWS, with a MongoDB database.

GLSL BLAS: GLSL code for non-complex BLAS operations with Vulkan. My final year masters project. Using modern C++ compile-time evaluation to validate shaders.

BLAS website: A website documenting BLAS operations. While working on GLSL BLAS I found the older website used to document BLAS to be a little uncomfortable, so I made this. I’ve also added some Python Manim animations to illustrate the operations.

Cogent: A simple library Rust library using ArrayFire for training simple neural networks; like a small Keras. A component of my final year bachelors project.

Genetic Draughts AI: My first ever venture into machine learning and optimisation. A simple tree C++ search program to play draughts using a genetic algorithm to judge board positions. I still remember the moment it beat me.