If you don't mind, could you drop some code? I'd be interested to see the result :)

sure, for example it generated this small demo of the type and contract safeguards. As you can see, it's mostly "Forth but with things":

  # bank.ax — The Safe Bank (Milestone 2)
  #
  # Demonstrates property-based verification of financial operations.
  # Each function has PRE/POST contracts. VERIFY auto-generates random
  # inputs, filters by PRE, runs the function, and checks POST holds.
  
  # DEPOSIT: add amount to balance
  # Stack: [amount, balance] (amount on top)
  # PRE: amount > 0 AND balance >= 0
  # POST: result >= 0
  DEF deposit : int int -> int
    PRE { OVER 0 GTE SWAP 0 GT AND }
    ADD
    POST DUP 0 GTE
  END
  
  # WITHDRAW: subtract amount from balance
  # Stack: [amount, balance] (amount on top)
  # PRE: amount > 0 AND balance >= amount
  # POST: result >= 0
  DEF withdraw : int int -> int
    PRE { OVER OVER GTE SWAP 0 GT AND }
    SUB
    POST DUP 0 GTE
  END
  
  # Verify both functions — 500 random tests each
  VERIFY deposit 500
  VERIFY withdraw 500
  
  # Prove both functions — mathematically, for ALL inputs
  PROVE deposit
  PROVE withdraw
  
  # Demo: manual operations
  1000 200 deposit SAY
  1000 300 withdraw SAY

Running it outputs:

  VERIFY deposit: OK — 500 tests passed (1056 skipped by PRE)
  VERIFY withdraw: OK — 500 tests passed (1606 skipped by PRE)
  PROVE deposit: PROVEN — POST holds for all inputs satisfying PRE
  PROVE withdraw: PROVEN — POST holds for all inputs satisfying PRE
  1200
  700

How does it do the proving?

Spawns and calls z3 under the hood, I did let it cheat there because otherwise it's rabbit holes below rabbit holes all the way down :)

thanks.

This is one of the more interesting uses of Claude I've seen. Instead of asking it to write code in an existing language, you asked it to design the language it wants to think in. There's something philosophically fun about that I feel = like asking a painter to design their ideal brush.

I'm curious whether the generated language actually makes Claude produce better/more reliable outputs when writing in it, or if it just reflects Claude's training bias toward what "good language design" looks like in its corpus. Would be a fascinating benchmark to run.

> There's something philosophically fun about that I feel = like asking a painter to design their ideal brush.

With the large difference that painters actually paint and use the brush, they don't just algorithmically regurgitate paintings they've been shown.

I plan to keep dumping tokens into it here and there to see where it goes, it's a fun rabbit hole.

I find that it's able to produce working code in the generated language just from the README and the previous examples without much trouble. And I've seen the strict typing help it catch and correct bugs quickly. I steer it very little. The only thing I keep an eye on is not allowing it to cheat about things like writing lots of concrete functionality in the host language and then just calling that from the interpreter.

If you want to go really meta ask Claude Code to re-implement itself in the new language. You could keep going doing this.

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...