sorins.uk 11 courses · 401 lessons

Down to the metal,
and back up to the proof.

Working notes, written out properly.

Each course starts from the smallest thing that is actually true — a reset vector, an instruction encoding, a single inference rule — and builds up from there. They read in order but stand alone, so start wherever the gap is.

Firmware

Before the operating system

Reset vectors, boot services, and the handover to a kernel.

/bios_tutor 39 lessons

BIOS Internals

From Bytes to Filesystems
Architecture

Instruction sets

Registers, modes, encodings, and the contract between hardware and software.

/x86_tutor 50 lessons

The x86 CPU

From Transistors to Linux
/x64_tutor 50 lessons

The x86_64 CPU

From i386 to Long Mode
/arm64_tutor 14 lessons

The ARM64 CPU

AArch64 — Reset to Userspace
/riscv_tutor 50 lessons

RISC-V

A clean-slate ISA, an assembler, an emulator
/sail_tutor 20 lessons

Sail

A spec that runs and proves — via a TPM 2.0 model
Systems

Building on the machine

What you write once the hardware hands over control — and what you write it in.

/osdev_tutor 39 lessons

OS Development

From Bytes to Filesystems
/nvim_tutor 65 lessons

Neovim

From Motions to Plugins

An interactive Neovim trainer: 65 lessons with a live in-browser editor, from basic motions through advanced editing, IDE features, and Lua plugin development.
Formal

Proving it correct

The other direction: from inference rules up to machine-checked proof.

/proof_theory_tutor 36 lessons

Proof Theory

From Judgments to Adjoint Logic
/lean_tutor 38 lessons

Lean 4 & Dependent Type Theory

A Field Guide
Also

Everything else

Pages that haven't been filed under a layer yet.

/elliptic_tutor

Elliptic Curves

From the Group Law to Rank Records

This course builds elliptic curve theory from first principles up to the machinery behind the 2026 rank-30 record. Nothing is assumed beyond…

Nothing matches that.