It kind of feels like it wants to go there or thereabouts, but to be honest, I just half understand half of the roadmap it has written for itself:

  - **v0.0.1** (complete): Interpreter, PRE/POST contracts, REPL, TIMES/WHILE, FILTER/MAP/REDUCE, strings, I/O
  - **v0.1.0** (complete): Static type checker, VERIFY (property-based contract testing), maps, Safe Bank milestone
  - **v0.2.0** (complete): PROVE — compile-time contract verification via Z3 SMT solver
  - **v0.3.0** (complete): Algebraic data types (TYPE/MATCH) — Option, Result, and user-defined sum types with exhaustiveness checking
  - **v0.4.0** (complete): JSON parser/encoder milestone — wildcard MATCH, string primitives, ROT4, PAIRS, NUM_STR, VERIFY for sum types
  - **v0.4.1** (current): PROVE for IF/ELSE branches (via SMT-LIB `ite`), ABS/MIN/MAX, function call inlining
  - **v0.5.0** (next): Practical language features — LET bindings, IMPORT/modules, error handling, standard library
  - **v0.6.0**: PROVE for MATCH/algebraic types, refinement-style reasoning
  - **v0.7.0**: Typed BEAM concurrency (typed message passing, stateful actors)
  - **v0.8.0**: BEAM bytecode compilation
  - **Future**: Declarative constraint solving, tensor/distribution primitives, multi-agent collaboration

I'd say the sky is the limit, but in fact the limit is the stingy token budget of the 20€ Claude sub...