Puffin for Racketeers

Puffin is a small Racket-family language. It began as a compilers-course project and was extended — with Claude Code — into a self-hosting compiler (native arm64 and x86-64 backends, plus a bytecode VM), gradual types over algebraic datatypes, and a file-based module system. The same compiler runs in the browser playground, compiled to bytecode on a WebAssembly VM. If you know Racket, most of Puffin will read as familiar; this tutorial walks the differences, each as a Racket/Puffin pair with a note on why it works that way. It is a young language with rough edges, and some of its design decisions are still open to second-guessing — those are called out where they come up rather than papered over.

Ten lines of typed Puffin — an interpreter, of course:

(define-type Expr
  (Num Int)
  (Add Expr Expr)
  (Mul Expr Expr))

(define (eval-expr [e : Expr]) : Int
  (match e
    [(Num n) n]
    [(Add a b) (+ (eval-expr a) (eval-expr b))]
    [(Mul a b) (* (eval-expr a) (eval-expr b))]))

(println (eval-expr (Add (Mul (Num 3) (Num 4)) (Num 1))))   ;; 13

Every example on this page is real: each one was run (and typechecked) with the toolchain in this repo, and error messages are quoted verbatim. Every example also pastes straight into the web playground, which runs the real compiler.

What carries over from Racket

Most of what you already know from Racket works unchanged:

only #f is false proper tail calls named let internal defines (letrec*-scoped) first-class closures quasiquote + splicing match interned symbols, eq?/equal?

A million-iteration loop in O(1) stack, exactly as you would write it in Racket:

(let loop ([i 0] [acc 0])
  (if (< i 1000000)
      (loop (+ i 1) (+ acc i))
      (println acc)))          ;; 499999500000

Hashes and sets: one immutable default

#lang racket
(define h0 (hash 'a 1 'b 2))    ; immutable
(define h1 (hash-set h0 'c 3))  ; functional update
(hash-count h0)                 ; 2 — h0 untouched
;; ...but pick your flavor: hash, hasheq,
;; hasheqv, make-hash, make-hasheq,
;; make-weak-hasheq, ...

(define h0 (hash 'a 1 'b 2))    ;; THE hash
(define h1 (hash-set h0 'c 3))  ;; a NEW hash
(println (hash-count h0))       ;; 2 — h0 untouched
(println (hash-count h1))       ;; 3
(println (equal? (hash 'x 1 'y 2)
                 (hash 'y 2 'x 1)))  ;; #t
(define m (make-hash))          ;; the tolerated
(hash-set! m 'hits 0)           ;; mutable variant
(hash-set! m 'hits (+ 1 (hash-ref m 'hits)))
(println (hash-ref m 'hits))    ;; 1

Racket and Puffin agree that immutable is the right default, but Puffin keeps exactly one flavor: (hash) is an eq?-keyed persistent HAMT in the native runtime — hash-set is O(log n) structural sharing, not a copy — and immutable collections compare by value under equal?. Mutation exists where you ask for it (make-hash, hash-set!), and those tables compare by identity. Sets (set/set-add, make-set/set-add!) follow the same story. Pairs are immutable, full stop: there is no set-car!.

Numbers: 61-bit fixnums only

(expt 2 100)  ; 1267650600228229401496703205376
(/ 1 3)       ; 1/3 — an exact rational
(sqrt -1)     ; 0+1i — the full tower

(println (* 1000000 1000000))  ;; 1000000000000
(println (quotient 7 2))       ;; 3 — checked division
(println (remainder 7 2))      ;; 1
;; no floats, no bignums, no rationals:
;; 61-bit fixnums are the numbers. Stay under ±2^60.

Puffin trades Racket's numeric tower for one unboxed machine representation: a fixnum fits in a tagged 64-bit word, so arithmetic compiles straight to machine arithmetic. That keeps the compiler and its data structures fast, but it is a genuine limitation — there are no floats, no bignums, no rationals, and code that needs them has to build them itself or reach across the FFI. There is also a seam between routes: native code and the bytecode VM share one 61-bit tagged representation, while the Racket-hosted reference interpreter uses arbitrary precision, so a program that overflows 2^60 can get different answers from the two. The type system does not close that seam — its casts check a value's shape, and an overflowed fixnum is still an Int. It is a real sharp edge, worth knowing about, even if course-scale arithmetic rarely reaches it.

Pattern matching

Everything you use in Racket's match is here, feature for feature: quasiquote patterns, ellipsis (including nested), clause guards with #:when, and ? predicate patterns. This runs unchanged in both languages (modulo #lang):

(define (analyze e)
  (match e
    [`(add ,a ,b) (list 'sum a b)]
    [`(lambda (,xs ...) ,body) (list 'fn (length xs))]
    [`(program (define (,ns ,ps ...) ,bs) ...)   ;; nested ellipsis
     (list 'defs ns (map length ps))]
    [(? fixnum? n) #:when (< n 0) 'negative]
    [(? fixnum? n) 'number]
    [_ 'other]))

(println (analyze '(add 1 2)))          ;; (sum 1 2)
(println (analyze '(lambda (x y z) x))) ;; (fn 3)
(println (analyze '(program (define (f a b) 1)
                            (define (g x) 2))))  ;; (defs (f g) (2 1))
(println (analyze -5))                  ;; negative
(println (analyze 7))                   ;; number

Under nested ellipsis each variable collects a list of its per-element matches, as in Racket — this is the idiom the Puffin compiler itself is written in. None of this differs from Racket; what differs is what you match on.

The same interpreter, two ways

(define (eval-expr e)
  (match e
    [`(num ,n) n]
    [`(add ,a ,b)
     (+ (eval-expr a) (eval-expr b))]
    [`(mul ,a ,b)
     (* (eval-expr a) (eval-expr b))]
    [`(neg ,a) (- (eval-expr a))]))

(println
 (eval-expr
  '(add (num 1)
        (mul (num 3) (neg (num 4))))))  ;; -11

(define-type Expr
  (Num Int)
  (Add Expr Expr)
  (Mul Expr Expr)
  (Neg Expr))

(define (eval-expr [e : Expr]) : Int
  (match e
    [(Num n) n]
    [(Add a b) (+ (eval-expr a) (eval-expr b))]
    [(Mul a b) (* (eval-expr a) (eval-expr b))]
    [(Neg a) (- (eval-expr a))]))

(println
 (eval-expr
  (Add (Num 1)
       (Mul (Num 3) (Neg (Num 4))))))   ;; -11

Both run in Puffin — the left one is also verbatim Racket. In the quasiquote version an expression is "whatever list shape the patterns happen to expect": any s-expression can leak in, and nothing owns the set of cases. In the ADT version, (Add a b) is a constructor pattern — match recognizes it because Add is bound as a constructor — and the type declaration is the single place the shape of expressions is defined.

The difference shows up in a single typo. Misspell a quasiquote tag and you get a clause that silently never matches — the program dies at runtime, on the input that should have worked. Misspell a constructor and the compiler stops you immediately, even when the bad clause is unreachable:

(define (f e)
  (match e
    [`(add ,a ,b) (+ a b)]
    [`(mull ,a ,b) (* a b)]))  ;; oops
(println (f '(mul 3 4)))

error: match-failure

(match e
  [(Num n) n]
  [(Add a b) (+ (eval-expr a) (eval-expr b))]
  [(Mull a b) (* (eval-expr a) (eval-expr b))])
;; Mull names no constructor in scope

error: match: no matching clause for '(Mull a b)

And because a module's define-types are a closed world (see modules), the compiler knows the complete constructor set of every ADT — which is what makes exhaustiveness checking possible at all.

Nullary constructors are bare names — and patterns nest

(define-type Shape
  (Point)
  (Circle Int)
  (Rect Int Int))

(define (classify [s : Shape]) : Sym
  (match s
    [Point 'point]              ;; bare nullary name: no (Point) noise
    [(Circle 0) 'degenerate]    ;; literals nest inside constructors
    [(Circle _) 'circle]
    [(Rect w h) #:when (eq? w h) 'square]
    [_ 'rectangle]))

(println (map classify
              (list Point (Circle 0) (Circle 9) (Rect 4 4) (Rect 4 2))))
;; (point degenerate circle square rectangle)

A nullary constructor is a value, not a function you call: Point, not (Point) — in expressions and in patterns alike, as in ML. A bare pattern symbol that names a nullary constructor matches that constructor; anything else stays a binder, exactly as before, so untyped code cannot change meaning.

Gradual types

Gradual typing is where Puffin departs most from both Racket and Typed Racket. Typed Racket's answer to "how do I type Scheme?" is a second language: a separate #lang, subtyping with unions, occurrence typing, contracts at module boundaries. Puffin's answer is one language in which the unannotated type is _ (Any) and annotations only ever tighten it. A whole program with no annotations typechecks as written.

Declaring types: define-type, implicitly mutually recursive

#lang typed/racket
(struct Leaf ([n : Integer]))
(struct Node ([f : Forest]))
(struct FNil ())
(struct FCons ([t : Tree] [rest : Forest]))
(define-type Tree (U Leaf Node))
(define-type Forest (U FNil FCons))

(: tree-sum (-> Tree Integer))
(define (tree-sum t)
  (match t
    [(Leaf n) n]
    [(Node f) (forest-sum f)]))
;; (forest-sum is symmetric)

(define-type Tree
  (Leaf Int)
  (Node Forest))     ;; Forest is defined BELOW — fine
(define-type Forest
  (FNil)
  (FCons Tree Forest))

(define (tree-sum [t : Tree]) : Int
  (match t
    [(Leaf n) n]
    [(Node f) (forest-sum f)]))
(define (forest-sum [f : Forest]) : Int
  (match f
    [FNil 0]
    [(FCons t rest) (+ (tree-sum t) (forest-sum rest))]))

(println (tree-sum
  (Node (FCons (Leaf 1)
        (FCons (Node (FCons (Leaf 2) FNil)) FNil)))))  ;; 3

One form declares the type and its constructors together — no struct-per-variant plus a union on the side. And there is no fix or and block for mutual recursion: all define-types in a module form one implicitly mutually recursive group, mirroring how top-level defines are already letrec*-recursive — types follow the same scoping rule as values. Parameterized types work the same way: (define-type (Option a) (None) (Some a)) gives Some : (-> a (Option a)) and None : (Option a).

Annotations anywhere, _ everywhere else

#lang typed/racket   ; the whole FILE opts in
(: area (-> Integer Integer))
(define (area r) (* pi* (* r r)))
;; ...and now EVERYTHING in this module
;; must typecheck. Mixing means module
;; boundaries and require/typed.

(: pi Int)                         ;; declaration form
(define pi 314159)
(define (area [r : Int]) : Int     ;; params + result
  (* pi (* r r)))
(define (mixed a [b : Int] c)      ;; any subset;
  (list a b c))                    ;; a, c default to _
(let ([xs : (List Int) (list 1 2 3)])
  (println (foldl (lambda ([x : Int] acc) (+ x acc))
                  0 xs)))          ;; 6
(println (ann (+ 20 22) Int))      ;; 42 — ascription
(println (area 2))                 ;; 1256636
(println (mixed 'anything 5 "goes"))

Every binding position takes an optional annotation — [x : t] formals, : result on defines, (: name t) declarations, [x : t e] in let, (ann e t) on any expression — and every omitted one is _. There is no typed/untyped module split to manage: the granularity of gradualness is the individual annotation, in one language, checked by one typechecker on every route — native, bytecode, the Racket oracle's interpreter, and the browser playground, which runs the same compiler.

Consistency, not subtyping

Where Typed Racket asks "is this type a subtype of that one?", Puffin's bidirectional checker asks Siek–Taha consistency: _ ~ τ and τ ~ _ for every τ, congruent componentwise on containers and arrows, and — crucially — not transitive: Int ~ _ and _ ~ Bool prove nothing about Int and Bool. Concrete-vs-concrete disagreement is a compile-time error:

(define (inc [n : Int]) : Int (+ n 1))
(inc #t)

error: typecheck: inc: argument has type Bool, expected Int [main.puf:2]

These are compile-time errors in the browser too: the playground's Run typechecks with the same checker before anything executes, so the red boxes in this tutorial reproduce verbatim in its output pane.

The other pillar of Typed Racket — occurrence typing, where (if (string? x) ...) narrows a union — has no analogue in Puffin, because there are no unions to narrow. Dynamic dispatch on predicates is what _ is for; statically known alternatives are what ADTs are for:

#lang typed/racket
(define (len-or-inc [x : (U String Integer)])
  (if (string? x)
      (string-length x)   ; x : String here
      (add1 x)))          ; x : Integer here

(define (len-or-inc x)    ;; x : _
  (if (string? x)
      (string-length x)   ;; _ ~ Str: allowed
      (+ x 1)))           ;; _ ~ Int: allowed
(println (len-or-inc "four"))  ;; 4
(println (len-or-inc 41))      ;; 42

This is a real trade: Typed Racket proves more about predicate-heavy code; Puffin keeps the theory small (one relation, no subtype lattice) and pushes you toward constructors, where the checker's answers are exact.

The gradual guarantee — and contracts vs hints

The design rule: unannotated code never fails to check. The entire untyped corpus — 297 of the 309 golden checks — passes under the checker unchanged; that is the regression suite for the claim. Making that true required one careful distinction inside applications. A formal's concrete structure is a contract — violate it and you get an error:

(car 5)

error: typecheck: car: argument has type Int, expected (Pairof a b) [main.puf:1]

But a constraint that exists only because inference greedily bound a type variable from a sibling argument is a hint, not a contract — a conflict there quietly demotes the variable to _ instead of erroring, because no annotation you wrote is being violated:

;; hash-set : (-> (Hash k v) k v (Hash k v))
;; the first argument binds v := Int; the third argument says Str.
;; v was inferred, not declared — so v demotes to _ and this checks:
(define h (hash-set (hash 'a 1) 'b "two"))
(println (hash-ref h 'b))   ;; two

Untyped Scheme programs are full of heterogeneous hashes and lists; treating inference guesses as contracts would break them, and then the type system would be opt-in after all. Only what you annotate constrains you.

(List a) and (Pairof a d): equi-recursive, no unions

;; cons : (-> a b (Pairof a b)) — so assoc pairs just work,
;; and (List a) unfolds on demand to (Pairof a (List a))-or-nil:
(define (lookup [ps : (List (Pairof Sym Int))] [k : Sym]) : Int
  (match ps
    ['() -1]
    [(cons (cons k2 v) rest) (if (eq? k k2) v (lookup rest k))]))

(println (lookup (list (cons 'a 1) (cons 'b 2)) 'b))  ;; 2
(println (lookup (list (cons 'a 1)) 'z))              ;; -1

In Typed Racket, (Listof a) relates to pairs through the subtype lattice. Puffin has no subtyping, so it gets the same effect equi-recursively: the consistency checker unfolds (List a) one step when it meets a Pairof, and '() : (List _). Proper lists and dotted pairs both get honest types, with neither unions nor a lattice in the theory.

Cast semantics — checked, then guarded

Types are checked, then every declared boundary is guarded with a transient (first-order) cast before annotations erase: annotated parameters check on function entry, declared results on return, and ann, annotated lets, and (: …) defines check their values. A failed cast is a precise runtime error carrying a blame label naming the boundary — cast: expected Int, got #t (blame: f's argument x) — instead of whatever tag check the value happened to hit later. Unannotated code gets no casts at all (it compiles byte-identically), so the gradual guarantee is free. Constructor instances have their own heap kind — not vectors — so (println (Some 1)) prints (Some 1) (a nullary constructor prints bare: None), (vector? (Some 1)) is #f, and adt? is the disjoint predicate.

Modules

Puffin takes Racket's discipline — a file is a module, with provide and require — and mixes in an SML sensibility: optional signature files, arity checking, and genuine separate compilation.

#lang racket   ; every file: a #lang module
(require "geometry.rkt"
         (prefix-in u: "util.rkt")
         (only-in "list.rkt" twice)
         (rename-in "old.rkt" [twice do-twice]))
(provide area)

;; no #lang line — a .puf file IS a module
(require "geometry.puf")
(require "util.puf" #:as U)          ;; qualified: U.twice
(require "list.puf" #:only (twice)
                    #:rename ((twice do-twice)))
(provide area)
;; no provide form at all = everything is exported

A complete two-module program (both files verified together):

;; ---- geometry.puf ----------------------------------------
(provide area perimeter)
(define pi 314159)                   ;; private: not provided
(define scale 100000)
(define (area r) (quotient (* pi (* r r)) scale))
(define (perimeter r) (quotient (* 2 (* pi r)) scale))

;; ---- util.puf --------------------------------------------
(provide twice)
(define (twice f x) (f (f x)))

;; ---- main.puf --------------------------------------------
(require "geometry.puf")
(require "util.puf" #:as U)
(println (area 10))                  ;; 314
(println (perimeter 10))             ;; 62
(println (U.twice (lambda (x) (* x x)) 3))   ;; 81

Differences from Racket worth knowing:

• Requires must form a DAG — cycles are a compile-time error naming the cycle. This is deliberate, not a limitation to route around: it gives a well-defined initialization order, it is what makes separate compilation's interface files possible, and it makes each module's types a closed world (the property exhaustiveness checking needs).
• Top-level effects run once, in depth-first postorder of the require DAG — dependencies before dependents, each module exactly once, however many paths reach it.
• Import collisions are errors, never silent shadowing: two modules providing the same name, or an import colliding with a local define, stops the compile — disambiguate with #:as or #:rename.

Signatures: .pufs files

;; ---- ring.pufs — a signature file -------------------------
(signature RING
  (val zero)          ;; a value
  (fun add 2)         ;; a function of stated arity
  (fun neg 1))

;; ---- int-ring.puf ------------------------------------------
(provide #:sig "ring.pufs")   ;; exports become EXACTLY the sig
(define zero 0)
(define (add a b) (+ a b))
(define (neg a) (- a))
(define (helper x) x)         ;; outside the sig: private

;; ---- main.puf ----------------------------------------------
(require "int-ring.puf")
(println (add (neg 3) zero))  ;; -3   ...but (helper 1) is
                              ;; "unbound id helper": narrowed away

Ascription checks that every signature name is defined and that fun arities match, and it narrows: names outside the signature are private even though they were defined. Racket's closest analogue is a contracted provide; the .pufs file is closer to an SML signature — a separable, client-readable interface. When you want none of this, write nothing: specs are optional all the way down. And separate compilation falls out: bin/puffin -c --separate main.puf -o prog compiles each module in the DAG to a cached .o + interface file and links, rebuilding only what changed.

Types across modules

Calling C (the FFI)

A foreign import is a typed declaration: the foreign form names a shared library and declares each function with the same (: name τ) syntax the type system already owns. The declared type does all the work — the checker types your call sites with it, and the runtime derives the marshaling from it (there is no way to write an unmarshaled call). Every output below is verbatim from real runs (native and the bytecode VM agree byte-for-byte):

(foreign "libSystem.B.dylib"
  (: c-abs (-> Int Int) #:c-name "labs")
  (: c-strlen (-> Str Int) #:c-name "strlen")
  (: c-getenv (-> Str (Nullable Str)) #:c-name "getenv"))
(println (c-abs -42))
(println (c-strlen "a puffin appears"))
(println (if (c-getenv "NO_SUCH_VARIABLE_SET") 'set 'unset))

42
16
unset

The pieces, briefly. The library loads (dlopen) when the module's top level runs — a missing library or symbol is a load-time error. #:c-name picks the linker symbol (default: the Puffin name with - → _). Marshallable types are Int (with width spellings I8…U64 for narrow C types), Bool, Str (borrowed out, copied in), Void results, opaque handle types, and (Nullable τ) results, which map C's NULL to #f so a null pointer never reaches your code as a bare word. A foreign name is an ordinary binding: procedure? says #t, it provides, and (map c-abs xs) works.

Opaque C pointers cross as foreign handles: declare the type with define-foreign-type and it becomes a branded, unforgeable heap kind — no user code can mint one from an Int, passing a Regex where a Sqlite is declared is a blamed cast error, and #:consumes marks the close function so use-after-close and double-close are loud errors instead of double frees. Here is the Puffin face over a Rust regex crate (tests/ffi-demo/pfregex in the repo — a cdylib with extern "C" exports is indistinguishable from a C library):

(define-foreign-type Regex)
(foreign "../target/release/libpfregex.dylib"
  (: regex-compile (-> Str (Nullable Regex)) #:c-name "pfregex_compile")
  (: regex-match?  (-> Regex Str Bool)       #:c-name "pfregex_is_match")
  (: regex-find    (-> Regex Str (Nullable Str)) #:c-name "pfregex_find"
                                                 #:gift "pfregex_str_free")
  (: regex-close   (-> Regex Void)           #:c-name "pfregex_free"
                                             #:consumes))
(define re (regex-compile "pu[f]+in"))
(println (regex-match? re "a puffin appears"))
(println (regex-find re "one pufffin, two puffins"))
(regex-close re)
(println re)

#t
pufffin
#<Regex closed>

#:gift names the deallocator for a malloc'd string result: the runtime copies the string and immediately frees the original through the library's own free function, so the two allocators never touch each other's memory. Forget to close a handle and the leak detector tells you at exit (puffin ffi warning: 1 foreign handle left open at exit: #<Regex>) — closing is still your job. And one honest limit: the browser has no dlopen, so the playground compiles FFI programs fine but refuses to run them at load, with exactly:

error: foreign library libpfregex.dylib is not available in the browser

A real guest: Z3 as a Puffin API

examples/z3/z3.puf binds the Z3 SMT solver (brew install z3) in two handle types and six imports — and the whole binding fits on one screen because the workhorse is Z3_eval_smtlib2_string: queries go out as SMT-LIB text, answers come back as text, and SMT-LIB is s-expressions. So queries are quasiquoted Puffin data (value->string renders them verbatim) and replies parse back into Puffin data with the ~30-line reader in the same file. There is no binding layer to learn; the boundary speaks your data:

(define-foreign-type Z3Config)
(define-foreign-type Z3Context)
(foreign "/opt/homebrew/lib/libz3.dylib"
  (: z3-mk-config   (-> Z3Config)           #:c-name "Z3_mk_config")
  (: z3-mk-context  (-> Z3Config Z3Context) #:c-name "Z3_mk_context")
  (: z3-del-config  (-> Z3Config Void)      #:c-name "Z3_del_config"  #:consumes)
  (: z3-del-context (-> Z3Context Void)     #:c-name "Z3_del_context" #:consumes)
  (: z3-eval        (-> Z3Context Str Str)  #:c-name "Z3_eval_smtlib2_string"))

(require "z3.puf")
(define ctx (z3-new))
(z3-send* ctx '((declare-const x Int)
                (assert (> x 41))
                (assert (< x 43))))
(println (z3-check-sat ctx))
(println (z3-get-values ctx '(x)))
(z3-close ctx)

sat
((x 42))

The elaborate version is examples/z3/sudoku.puf: it generates a Sudoku's whole constraint system as data — 81 declare-consts, 27 distincts over rows/columns/boxes built with ordinary map and append-map, the givens — hands it to Z3, reads the model back, and prints the solved board. Then it asserts the negation of the model and asks again: unsat, so the solution is provably unique. The tail of a real run (native and the bytecode VM agree):

$ build/puffincc examples/z3/sudoku.puf -o sudoku && ./sudoku
...
solution:
5 3 4 | 6 7 8 | 9 1 2
6 7 2 | 1 9 5 | 3 4 8
1 9 8 | 3 4 2 | 5 6 7
------+-------+------
8 5 9 | 7 6 1 | 4 2 3
4 2 6 | 8 5 3 | 7 9 1
7 1 3 | 9 2 4 | 8 5 6
------+-------+------
9 6 1 | 5 3 7 | 2 8 4
2 8 7 | 4 1 9 | 6 3 5
3 4 5 | 2 8 6 | 1 7 9
unsat
unsat above = the solution is unique

All the examples live in examples/ with golden outputs; tools/test-examples.sh runs them on both self-hosted routes (z3 ones skip, not fail, when libz3 is absent).

The full design — the marshaling table, the blame discipline, C++ and Rust guest rules, and what stays out (floats, callbacks, struct marshaling) — is docs/FFI.md.

Run it yourself

The compiler is puffincc — written in Puffin, compiled by Puffin, byte-stable at its own fixpoint — with three backends: arm64, x86-64, and bytecode for the VM:

bin/bootstrap                    # Racket-free bootstrap from the committed
                                 # bytecode seed (or bin/build-puffincc via
                                 # the Racket oracle), then:
build/puffincc prog.puf -o prog  # compile + link natively, or...
build/puffincc -t bytecode prog.puf -o prog.pbc   # ...compile to bytecode
bin/puffin-vm prog.pbc           # and run it on the native VM
build/puffincc -O 2 prog.puf -o prog   # optimization levels 0 / 1 (default) / 2

tools/gen-web-vm.sh              # build the browser engine artifacts, then:
(cd web && npm run dev)          # the playground: puffincc in wasm

bin/puffin prog.puf              # the Racket-hosted oracle: compile + run
bin/puffin -i prog.puf           # ...or interpret (same typechecker runs first)
bin/puffin                       # REPL (,help ,env ,quit)
bin/puffin -c --separate main.puf -o prog   # separate compilation + link

Module programs work everywhere a single file does — point any route at the entry file and the require DAG resolves from disk. -O1 (the default) is cp0-style contraction and bounded inlining plus safe open-coding of data-structure primitives; -O2 adds an AAM-based interprocedural analysis and its clients.

The zero-install route is the web playground under web/ — and it is not a JavaScript approximation of the language: it runs puffincc itself, compiled to bytecode, on a WebAssembly build of the bytecode VM. Run typechecks and compiles the editor source with the real compiler (the type errors quoted in this tutorial appear in the output pane), file tabs turn the editor into a module DAG, and the REPL is a persistent VM session: defines persist across evals, redefinition replaces, cross-eval mutual recursion and define-type work — until you press Reset session. Emacs keybindings, Cmd/Ctrl+Enter to run — every example in this tutorial pastes straight in. The standard library reference lives at stdlib.html — every function, categorized and typed, with a machine-verified example each.

Going deeper: the standard library reference (every function, with verified examples), docs/LANGUAGE.md (the day-to-day reference), docs/TYPES.md (the type system design), docs/MODULES.md (modules and separate compilation), docs/OPTIMIZER.md (the three optimization levels), docs/BYTECODE.md + docs/WASM-VM.md (the bytecode VM and the browser architecture), and bench/report.html (benchmarks against Racket — the wins and the losses both).