Puffin: Scheme-like language with self-hosting compiler and gradual types

azhenley1 pts0 comments

Puffin โ€” a small, self-hosting functional language

๐Ÿง<br>Puffin

A minimal Scheme/ML-like functional language โ€” self-hosting<br>compiler, gradual types, modules, and a typed FFI.

โ–ถ Try it in your browser<br>Puffin for Racketeers<br>Quick start<br>Source on GitHub

Puffin is a minimal Scheme/ML-like functional programming language<br>written by Claude Code, directed by (and extending a compiler written<br>by) Kristopher Micinski. The original compiler / language is detailed<br>here:<br>https://kmicinski.com/functional-programming/2025/11/23/build-a-language/<br>I used Claude Code to build Puffin by extending that teaching-focused<br>language (from Jeremy Siek's compiler book) with several<br>quality-of-life features:

Match patterns and quasiquoting

A gradual type system using consistency-based typing

A simple standard library consisting of sets, hashes (dictionaries),<br>and several other facilities

A simple module system inspired by SML

A typed FFI

The project is, in some ways, an adventure in Slop. My ultimate goal<br>is to use this to replace Racket for my day-to-day brainstorming in<br>compiler / interpreters / etc. Claude Fable built the code, I read all<br>of the code and understand the compiler's structure--but there are<br>still some serious gaps which have not been fully thought-through:<br>gradual typing, modules, these are places which are seriously<br>prototypical so far. I have written (again, using Claude Code) some<br>large ports of Racket applications into Puffin, and a translation of a<br>large (~10kloc) Racket application did demonstrate a serious Puffin<br>compiler bug--so there are surely both (a) genuinely bad, unsound<br>design choices which must be rooted out and (b) bugs in the<br>implementation.

Here's a "hello world" example:

(define-type Expr<br>(Num Int)<br>(Add Expr Expr)<br>(Mul Expr Expr))

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

(println (eval-expr (Add (Mul (Num 3) (Num 4)) (Num 1)))) ;; 13<br>The compiler is called puffincc : it is self-hosting, written in<br>Puffin (see puffincc-src/), and includes with three backends: (a)<br>arm64, (b) x86-64, and (c) bytecode. It is the single source of ground<br>truth for the language: the browser playground (web/) runs puffincc<br>itself, compiled to bytecode, on a WebAssembly build of the bytecode<br>VM (src/vm/).

Some highlights coming from Racket:

Self-hosting, Racket-free : bin/bootstrap builds the compiler<br>from the committed bytecode seed with nothing but a minimal C<br>toolchain (why not Rust!?), and should yield a stage-2/3<br>byte-identical fixpoint every time.

Gradual types are described in docs/TYPES.md: ADTs,<br>annotations where you want them, _ where you don't; transient<br>casts with blame at declared boundaries; exhaustiveness warnings.

A typed FFI (docs/FFI.md): dlopen'd C imports declared with<br>ordinary (: name ฯ„) types; the declaration generates the<br>marshaling, and every crossing is checked with blame naming the<br>import. As an example, examples/z3/ binds the Z3 SMT solver as a<br>Puffin API.

Modules + separate compilation described in docs/MODULES.md, a native<br>REPL, a bytecode VM, and the in-browser playground with the real<br>compiler and REPL.

Tested by construction : a 309-check golden corpus and a<br>differential error corpus run every program down every route โ€”<br>diagnostics byte-identical, rejection behavior corpus-tested like<br>success.

Quick start

bin/bootstrap # Racket-free bootstrap: cc-only, from<br># the committed seed boot/puffincc.pbc,<br># with a stage-2/3 fixpoint proof<br>build/puffincc prog.puf -o prog # puffincc compiles + links natively<br>build/puffincc -t bytecode prog.puf -o prog.pbc # ... or to bytecode<br>bin/puffin-vm prog.pbc # run bytecode on the native VM<br>tools/test-corpus.sh # the golden corpus, Racket-free<br># (`gen` mode WRITES the goldens)<br>tools/test-errors.sh # the differential ERROR corpus<br># (src/errors-corpus): must-fail<br># programs x every route<br>tools/test-examples.sh # the examples/ programs vs their<br># goldens, native + VM (z3 examples<br># skip when libz3 is absent)<br>tools/gen-web-vm.sh # browser engine artifacts (self-hosted)<br>(cd web && npm run dev) # the playground: puffincc in wasm<br>bin/refresh-boot # refresh the seed at release points<br>Multi-file programs use the module system ((require "lib.puf") /<br>(provide ...)); all backends (native, the bytecode VM, the web<br>playground) resolve via puffincc's resolver.

Documentation

There is a tutorial here:<br>docs/tutorial.html, Puffin for Racketeers. We (me and mister Claude) also wrote reference docs:

docs/LANGUAGE.md โ€” the language, day to day

docs/TYPES.md โ€” the gradual type system

docs/MODULES.md โ€” modules and separate compilation

docs/FFI.md โ€” the FFI, with runnable

examples/ (including the Z3 binding and a<br>solve-and-prove-unique Sudoku)

docs/STDLIB.md โ€” the standard library<br>(docs/stdlib.html is the generated reference; its examples are<br>executed and asserted at generation time)

docs/OPTIMIZER.md โ€” -O 0|1|2

docs/WASM-VM.md + docs/BYTECODE.md<br>โ€” the...

docs puffin expr compiler language bytecode

Related Articles