Skip to main content

Tutorials

Longer, step-by-step builds. Each tutorial produces a runnable program and teaches a coherent slice of the language. They are designed to be read in any order — each one lists its prerequisites and covers one conceptual slice well.

Prerequisites for all tutorials: Installation and Language tour.

Looking for short task-oriented snippets? See Cookbook.

Picking a track​

If you want to learn…Start with
The language end-to-end via a small projectTyped CLI tool
Refinement types and SMT verificationRefinement types
Pattern matching, match, active patternsPattern matching
Protocols and trait-like generic programmingProtocols
Context injection (DI)Context system
Async runtime, nursery, selectAsync pipeline
Memory model and the three-tier reference systemMemory safety
Building a non-trivial program (parser, ML)Parser / Small NN

For beginners​

Build a typed CLI tool — 30 min​

Build a small command-line log analyser that reads a config file and emits a JSON report.

Pattern matching — 30 min​

Walk through every form of pattern matching by writing a tiny Scheme interpreter: lex, parse, evaluate.

For type-theory​

Refinement types — 45 min​

Implement a ring buffer whose invariants — non-empty, bounded, sorted — are checked by the SMT solver at compile time, not at runtime.

Protocols — 45 min​

Build a small serialisation framework: define a Serialize protocol, implement it for core types, derive it for user types.

For applications​

Build a verified HTTP service — 60 min​

A tiny URL shortener with refinement-typed routes, context-injected storage, and structured concurrency.

  • Teaches: routing, refinements, nursery, Semaphore-bounded workers, testing with provided mocks, @verify(formal) with loop invariants.
  • Assumes: CLI tutorial (for project structure).
  • See also: cookbook/http-server, language/async-concurrency.

Context system — 30 min​

Take an existing function and progressively refactor it from implicit-global-state to fully-explicit using [...].

  • Teaches: context, provide, conditional contexts (if cfg.feature), named/aliased contexts, negative contexts for purity proofs.
  • Assumes: CLI tutorial.
  • See also: language/context-system, stdlib/context.

For libraries​

Write a parser from scratch — 45 min​

Combinator-style parsing for a small arithmetic DSL.

  • Teaches: function types, Maybe-based success/failure, combinator composition, recursive AST with Heap<T>, property testing.
  • Assumes: generics, patterns.
  • See also: cookbook/regex, language/functions.

For systems​

A verified data structure — 60 min​

Implement a sorted list and prove the sort invariant with @verify(formal).

Memory safety — 45 min​

Build a self-referential data structure (a doubly-linked list) three times: with &T (tier 0 default), with &checked T where escape analysis admits it, and with &unsafe T where you write the proof obligation yourself.

For concurrency​

An async pipeline with backpressure — 55 min​

Fan-out-fan-in with bounded channels, retry logic, and graceful shutdown on a kill signal.

For ML / numerics​

Train a small neural net — 45 min​

MNIST classifier using math.nn with autodiff.

  • Teaches: tensors, static shapes, autodiff::value_and_grad, nn::Linear, AdamW, training loop, shape verification via dependent types.
  • Assumes: refinement types are helpful but not required.
  • See also: stdlib/math, cookbook/shape-safe.

What's next after tutorials?​