Tyu
A systems programming language that makes program structure and correctness easier to examine.
- Drawn by
- Lex
- Date
- 2025-12
- Scale
- 1 : 1
- Sheet
- 01 OF 05
- A language built around a stack of values, with the types and arrangement checked before the program runs.
- Builds for x86_64, ARM, and RISC-V, both under an operating system and directly on hardware.
- An optional verification pipeline sends mathematical statements about the program to Lean 4, a proof assistant, and reports which remain unproved.
- A practical book and browser playground help people learn the language through examples.
Scroll across the drawing to see the detail.
Tyu asks how much we can understand about a systems program before running it. The work brings a language, its compiler, a verification pipeline, and teaching material together. It’s the project I’m most interested in supporting over the long term.
A language you can reason about§
Tyu is concatenative: programs combine small operations that take values from a stack and put results back. The compiler checks the types and shape of that stack. Contracts describe conditions a piece of code expects and promises; tracked effects make operations such as hardware access explicit.
Memory is allocated within defined regions, without a garbage collector. The toolchain builds programs for an operating system or for bare hardware, including x86_64, ARM, and RISC-V targets. Execution tests use QEMU, a machine emulator, to run built programs.
What proof checking means here§
The optional verification pipeline produces proof obligations: precise statements that need to be established for particular program properties. A Lean 4 integration checks proofs and reports obligations that remain open.
This is a way to bring mathematical checking into the build process. It isn’t a claim that every property of every Tyu program has been proved. The project documentation describes the pipeline and its scope.
Building the learning path too§
A language needs a way in. Assembling in Tyu connects the language and its standard library through practical labs. The browser playground lets you explore examples without installing the toolchain, and the book provides the longer path.
For me, this is a connected piece of work: design the language, build the tools, and explain the ideas well enough that someone else can use them.