Theme

Programming language

Tyu

A small, statically typed, concatenative systems language. Programs are built from words that transform a data stack — and nearly everything written down about a word is a machine-checked claim, not a comment. The book’s labs run right here on this site — no install required.
Try it in your browser Read the book

Safety is not the brake — it’s the engine. The rigor is what licenses the daring parts.

— Assembling in Tyu, Chapter 1 — The Rigor Is the Engine

Tyu targets the bare metal: freestanding images, MMIO, interrupt handlers on a budget, tasks and channels the platform provides. The toolchain checks the claims as you write — types make illegal values unrepresentable, contracts are promises the machine reads, effects are declared and discharged, and the developer-proof pipeline turns a program’s obligations into goals a proof assistant closes. When the checks pass, the daring parts are simply safe.

# Install

The toolchain is optional — the browser REPL needs nothing but a tab. To work natively, build from source — Rust via rustup, no other prerequisites:

Clone and build the Tyu toolchain

git clone https://github.com/lexbity/tyu.git
cd tyu_lang
cargo build --release -p langc -p tyu -p lmod-pack -p lmod-sign -p lmod-encrypt
export PATH="$PWD/target/release:$PATH"

The full tiered setup — hosted-first toolchain, QEMU for the metal interludes, and the smoke fixture that proves your first build — is Appendix C and the repository’s SETUP.md .

# Try it

  1. Run a lab in your browser — no install

    Open the browser REPL : a CodeMirror editor with a Tyu grammar, the book’s labs preloaded as one-click examples, an interpreter and a wasm32 backend, and a debug console. Start with Lab 1.1 — hello, checked.

  2. Write your first module

    A Tyu program is a stack of promises. Start with the ten-minute first chapter: your first .mod file, langc --emit=tc, and the first red/green lab.

  3. Run the labs natively

    Every chapter ships green labs (should compile and run), red labs (must be rejected, with the exact error), and engine labs (the checker itself). The fixtures live in the repository under docs/book/labs/ and are mirrored under /book/labs/ on this site.

  4. Prove something

    Chapter 14 walks the developer-proof pipeline: obligations harvested from your contracts, discharged with the pinned Lean toolchain.

# Read the book

Assembling in Tyu — draft v3 — is the documentation. Every lab real, every transcript verbatim, written in the open:

No install

The Browser REPL

Write and run Tyu in your tab: editor, checker, interpreter, wasm32 backend, and the book’s labs as one-click examples.
Appendix A

Language Reference

The built-in words, lexical syntax, types, declarations, and contracts.

# What it offers

Machine-checked claims

Types, contracts, and effect declarations are checked by the compiler — nearly everything written down about a word is a claim the machine verifies.

Concatenative and small

Words compose on a data stack; the stack has a shape, and the shape is checked.

Bare metal first

Freestanding images, MMIO descriptors, ISR budgets, and a cross-context rule for shared state — the platform is the target, not an abstraction over it.

The proof pipeline

A developer-proof pipeline harvests obligations from contracts and closes them with a proof assistant; the machine is witness.

Labs with real transcripts

Every lab is red/green/engine with verbatim toolchain output — if a transcript says the checker refused, it did.

QEMU verification

Emulation in verification: the machine as witness, from hosted fixtures to LM3S6965 boards.

Tyu is in open beta

The toolchain, the book, and the labs move together. Watch the repository, read the book , and try the labs — the transcripts are real, and that is for you to judge.
Tyu on GitHub Changelog