✓
MVP — Surface the verified kernel
Move the PRODUCT spine from prototype → MVP: surface the already-verified kernel's capabilities end-to-end (surface syntax → elaborator → run/#guard), so the language is one you can write real programs in. The bridge's first usable span (proof → programmable language); agent-observable write→run→verify loop. Kernel work is demand-driven — only when a tracer bullet can't be done in the shell. Deep verification-surfacing (state+check properties) is post-v1.
complete
✓
Tokenizer
DONE ✓ — pulled: strings · recursion · termination-checking. examples/tokenizer.bang runs.
complete
○
Parser-combinator library
THE next milestone — the acceptance test for polymorphism. Pulls: higher-order (compose, the ICTy re-rep) · generic data (Parser a). The tokenizer's generalization; retires its #50 mono limit. See docs/roadmap/project-roadmap.md.
no issues yet
▸
Spreadsheet (reactive dataflow)
Next candidate — lights up REACTIVITY (=, the distinctive dormant feature; mechanism already proven). Same shape as incremental compilation.
1 open issue
○
Key-value store (STM)
Wishlist — exercises STM (the one privileged primitive); full payoff needs post-v1 concurrency.
no issues yet
○
Web server
Wishlist — network-effect · STM/concurrency · capability-per-connection. More effect-shaped than a game; stresses the OS/distributed northstar.
no issues yet
○
Graphics (2048)
Wishlist — FFI-as-effect (raylib, Q37) · effectful recursion (#48). The first interactive-graphical program.
no issues yet
○
OS / distributed
Northstar — hardware FFI · scheduling-as-effect · capability isolation. Effects ARE the OS abstraction.
no issues yet