Avatar
  • Manchester, UK
  • 16:47 (UTC +01:00)

Toby Jordan

Self-Taught Programmer and Philosophy & RS Graduate

I am a self-taught programmer and will graduate this year with a First Class degree in Philosophy and Religious Studies from the University of Manchester, UK. I have always been passionate about computers, and started programming at 10 years-old.

I am proficient in Typescript, Python, and Odin. I have built full-stack type-safe web applications in Typescript using a modern tech stack including SvelteKit and Svelte 5, as well as low-level applications in Odin. See below for examples of my work.

At the moment, I am exploring Lambda Calculus and Type Theory in a series of blog posts. The first post walks through my implementation of a lambda calculus interpreter in Odin. The second post implements STLC and PCF, and discusses the Curry-Howard correspondence. In the third and final post, coming soon, I discuss the Lambda Cube and implement the Hindley-Milner type system.

My philosophy background shapes how I think about software: I am drawn to complex and foundational problems: type systems, language design, etc.

I am currently seeking a junior/intern software engineering role. Based in the UK; open to remote.

Projects

What I've been working on recently

  • Lemuria

    A social platform built around two-sided friendships, shelves, and topic-based boards. Inspired by Letterboxd and early Facebook.

    Bun · TypeScript · Hono · Drizzle · Svelte 5 · SvelteKit

  • Camel.py

    A reactive SPA framework for Python. Camel compiles a Python UI description to a typed intermediate representation, then interprets it with a small vanilla JS runtime.

    Python · JavaScript

  • Kaworu Linux

    A minimal NixOS rice built around Hyprland, Home Manager and Stylix. Declarative, reproducible, and opinionated — the entire system is defined in a single flake.

    NixOS · Nix · Hyprland

Blog

Writings on technology, philosophy, and their intersection

  • Types as Propositions, Proofs as Programs: Implementing STLC and PCF
    type theory · lambda calculus · odin · curry-howard

    We extend our lambda calculus interpreter with a type system, discover that almost nothing from the untyped standard library survives, derive PCF from first principles, and arrive somewhere unexpected: the typechecker we wrote is also a proof checker - Curry-Howard isomorphism.

  • Building a Lambda Calculus Interpreter in Odin
    lambda calculus · odin · interpreters · programming languages

    Lambda calculus has three rules, and yet booleans, arithmetic, linked lists, and recursion fall out of them. This is an account of building an interpreter for it in Odin - and of the theory that ambushes you along the way.

  • See all →