chris256.com July 2026
_ _ ____ ____ __
___| |__ _ __(_)___|___ \| ___| / /_ ___ ___ _ __ ___
/ __| '_ \| '__| / __| __) |___ \| '_ \ / __/ _ \| '_ ` _ \
| (__| | | | | | \__ \/ __/ ___) | (_) | (_| (_) | | | | | |
\___|_| |_|_| |_|___/_____|____/ \___(_)___\___/|_| |_| |_|
Christopher Lang's Personal Website
________________________________________________________________________________
About me
--------
I'm interested in theoretical computer science and systems engineering.
,
\`-._ __ My online presence:
\\ `-..____,.' `.
:`. / \`. github
: ) : : \ linkedin
;' ' ; | : youtube
).. .. .:.`.; :
/::... .:::... ` ;
; _ ' __ /:\ Interests we may share:
`:o> /\o_> ;:. `.
`-`.__ ; __..--- /:. \ operating systems
=== \_/ ;=====_.':. ; FPGA development
,/'`--'...`--.... ; formalising computer architecture
; ; text editors
.' ; voxel-based 3D rendering
.' ; writing video games in assembly
.' .. , . ; molecular dynamics software
: ::.. / ;::. | typesetting software
/ `.;::. | ;:.. ; chess engines
: |:. : ;:. ; building computer hardware
: :: ;:.. |. ; computer networking
: :; :::....| | generative image models
/\ ,/ \ ;:::::; ;
.:. \:..| : ; '.--| ;
::. :'' `-.,,; ;' ; ;
.-'. _.'\ / `; \,__: \
`---' `----' ; / \,.,,,/
`----`
click here for jotto (works best on mobile)
Project Showcase
----------------
________________________________________________________________________________
ArchSem Lean October 2025 - June 2026
This was my final-year dissertation project studying computer science at the
University of Cambridge. My supervisors were:
- Thibaut Pérami
- Léo Stefanesco
- Peter Sewell
> At the frontier of research into formalising multi-core CPU architecture
> specifications is ArchSem, a framework for writing machine-verified proofs
> against an architecture. Since ArchSem’s inception in 2021, it has been
> developed in the Rocq theorem proving language, but limitations in Rocq’s
> ecosystem, language design and performance have seriously hindered ArchSem’s
> progress. My project aims to port ArchSem to Lean, a newer theorem proving
> language that appears to solve many of the issues faced in ArchSem’s Rocq
> implementation.
TODO: explain this
[1] https://github.com/rems-project/archsem
[2] https://github.com/rems-project/archsem-lean
[3] ArchSem in Lean Dissertation
________________________________________________________________________________
Writing Lean Kakoune October 2025
Lean is a theorem proving language.
Kakoune is a vim-like (but better) text editor.
Do you want to use Kakoune to write Lean? I have got your back.
I added support for the lean goal view in the kak-lsp [1].
And I wrote a Kakoune plugin for Lean [2].
[1] https://github.com/kakoune-lsp/kakoune-lsp/pull/860
[2] https://github.com/Chris-F5/kakoune-lean
________________________________________________________________________________
2026 Cambridge Game Jam March 2026
This was my submission for the 48-hour 2026 cambridge game jam. In previous
years, I participated in the game jam and wrote my game in assembly. This year
I wanted to go even "lower-level". So this submission is written in Verilog and
runs on an Nexus A7 T100 development board equiped with an AMD Artix 7 FPGA.
This is my first time properly using verilog, the idea was that I'd use the game
jam as an oppotunity to learn a hardware description language.
Video output is generated with my custom graphics pipeline and sent to the VGA
driver which was also written during the jam. There is no framebuffer, instead
I generate pixels in a 36-stage pipeline clocked at 25MHz, the same frequency
pixels are output on VGA. Pixels leaving the pipeline are sent directly to VGA
in a kind of "just-in-time" rendering of individial pixels. The pipeline looks
something like this:
1. Predict screen_coords that will need to be sent on VGA in 36 cycles.
2. Model,view,projection matrix applied.
3. 2 divisions convert from homogenous to non-homogenous plane xy coordinates.
4. Plane coordinates convert to 'cube' hexagonal coordinate system.
5. Hexagon coordinates converted to color by inspecting game state.
Keyboard input is read from a PS2 keyboard driver. I use a modified version of
Digilent's keyboard demo [3].
[1] https://github.com/Chris-F5/fpga-hexagon-video-game
[2] https://www.youtube.com/watch?v=jnG2rAN-wWk
________________________________________________________________________________
Writing Video Games in Assembly 2022 - 2025
I enjoy writing video games in assembly (the images below are clicky).
Pong (2022) 
I wrote this pong clone in x86_64 asm using the linux framebuffer for graphics.
Lazer Recoil (2024) 
This game was written on 16-bit x86 and runs on MSDOS systems. It uses mode 13h
for graphics. It was written for the 48-hour 2024 Cambridge game jam.
Buckets (2025) 
This was my submission for the 2025 Cambridge game jam. Its a 2-player online
multiplayer which runs nicely on modern linux system by speaking to the X11
server for graphics and user input. I later split this X11 client logic out
into a dedicated x86_64 X11 client library [1].
[1] https://github.com/Chris-F5/x86x
________________________________________________________________________________
DPLL (Propositional Logic) Sodoku Solver Febuary 2025
I wrote then to help me internalise concepts I'm learning in a course on logic
and proof (Cambridge IB 2425) and to help me learn OCaml.
Davis-Putnam-Logeman-Loveland DPLL is a propositional logic algorithm to find an
interpretation that satisfies an expression. For example, you might ask it to
find an interpretation for
(X OR Y) AND (NOT (X AND Y))
and it might tell you that
{X=true, Y=false} entails (X OR Y) AND (NOT (X AND Y)).
We express a sodoku problem as a propositional logic statement of 9*9*9=729
variables where proposition P(i,j,n) is true iff the cell with coordinates (i,j)
holds the number n in the solution. Here i,j,n are elements of {1..9}. Then we
ask DPLL to find a solution.
[1] https://github.com/Chris-F5/dpll_sodoku
________________________________________________________________________________
Molecular Dynamics December 2025
In the winter of 2025 I was interested in writing molecular dynamics simulations
I[1]. t is a very technically interesting problem I would like to return to but
II find am limited by my lack of physics and chemistry knowledge.
I've animated energy minimization of water in a periodic system [2] and
evolution of the schrodinger equation using finite difference method in a
square well [3].
If you look closely in [2]'s energy minimization. You will see that the
molecules wiggle back and forth instead of converging to a low energy state.
I wont get into the details here, but to solve this I planned to implement the
ewald sum which I found very mathematically challenging.
[1] https://github.com/Chris-F5/molecular_dynamics
[2]:
[3]:
________________________________________________________________________________
SinGAN Generative Image Model April 2025
I have been exploring generative image models which can be trained on a single
image. I have been replicating the results of some influential papers including:
SinGAN Shaham 2019
Learning a Generative Model from a Single Natural Image
https://arxiv.org/abs/1905.01164
Here is my implementation and some results:
https://github.com/Chris-F5/generative_image_models
As you can see, it works much better for some images than for others.
Training Image Generated Image
________________________________________________________________________________
IP over rclone April 2025
The normal networking stack usually looks something like this:
Application/TCP/IP/Ethernet
But with the help of this project we can make it look like this:
Application/TCP/IP/Google Drive/TCP/IP/Ethernet
(at the cost of some performance). Using this we can make two distant computers
appear to be on the same local network through their shared connection to a
Google Drive folder (or any other cloud storage provider supported by rclone).
Essentially its a python script which creates a virtual network interface Linux
only). Then it handles the transport of IP packets to and from this interface
by invoking rclone commands which upload and download IP packets from a shared
cloud storage location.
[1] https://github.com/Chris-F5/ip_over_rclone
________________________________________________________________________________
Voxel Renderers April 2021 - September 2023
I was inspired by John Lin's voxel renderers [1] and the Teardown video game [2]
(before its release) to write a voxel renderer. This began a multi-year project
in which I wrote a number of renderers [3,4,5] exploring novel techniques for
rendering voxels. I really enjoyed the C+Vulkan workflow, although it was not
great for fast prototyping and iteration.
[1] https://www.youtube.com/@johnlin9665/videos
[2] https://teardowngame.com/
[3] https://github.com/Chris-F5/CppVulkanVoxelRaycaster
[4] https://github.com/Chris-F5/VoxelRenderer
[5] https://github.com/Chris-F5/lime
________________________________________________________________________________
Raspberry-Pi Operating System From Scratch (PIFS) 2023
I was inspired by the linux from scratch (LFS) project [1] to write a similar
guide to describe how to cross compile a linux-based operating system from
scratch (without relying on a distribution) for a Raspberry-Pi.
The guide [2] and its report [3] were submitted for my second A-Level EPQ which
recieved an A* grade.
If you want to follow the guide then email me.
[1] https://www.linuxfromscratch.org/lfs/
[2] PIFS guide
[3] PIFS report
________________________________________________________________________________
My Hardware
https://github.com/Chris-F5/28C256-EEPROM-programmer
https://youtu.be/iLvzs8jNgJo
https://youtube.com/shorts/ZYFhF9284ho
https://github.com/Chris-F5/rp2040_micropython_ov7670_driver
EEPROM Programmer (2022) 
6502 Computer (2023) 
ESP32 Dev Board(2023) 
Camera Driver (2024) 
RP2040 Apriltag Recognition (2024) 
________________________________________________________________________________
Typesetting Software November 2023
My computer science GCSE course required I undertake a programming project of
my choice. After spending some time messing around with procedural generation
of pixel art trees [3]. I eventually decided to write a typesetting software
in C [1]. I implemented a PDF library, font parsing library, and "line break
optimizer" all from scratch. It supported contents pages, footnotes, images etc
and the final report that I submitted to examiners [2] was itself formatted with
my typesetting software.
I guess the examiner liked it since my GCSE grade was one of the top 50 in the UK.
Later at university, I formatted most of my supervision work with this software.
[1] https://github.com/Chris-F5/typewriter
[2] report PDF
[3]:
________________________________________________________________________________
Chess Engines October 2020
One of my first programming projects was writing a chess engine in C#. This
was before I knew about git or backups so that code is lost now. From what
I remember, it was a simple minimax engine with no alpha-beta pruning and a
handwritten evaluation function.
When I was a GCSE student my computer science teacher suggested I do A-Level EPQ
(examined project) a few years early. For this project I wrote a chess engine
in rust [1]. It had alpha-beta pruning, variable depth, evaluation with piece
square tables and connected to a large endgame database. I manually tested it
against the lichess chess engines and it seemed roughly even with the engines
rated 1300-1500 (and it could beat me fairly consistency).
The EPQ recieved a grade A.
Since then I have played around a little with an engine based on bitboards [2]
but nowadays I prefer to work on software that does useful things.
[1] https://github.com/Chris-F5/ChessEngine
[2] https://github.com/Chris-F5/clce
________________________________________________________________________________
[email protected]