So I have been prodding Claude Code for a few sessions to actually do it. It's a silly experiment, but fun to watch. Right now it's implementing a JSON parser in the generated language as a kind of milestone example.

  # 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

  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

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.

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

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.

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

English is fine, but I am personally a lot faster in my mind and fingers and IDE with a language suited for this stuff. AI guys just want to be teachers deep down I think :).

> Working atari 2600 flappy bird, by just asking chatgpt to directly output the raw bytes for a cartridge image

TBH this is a bit unexpected: it should know how to encode instructions, of course, but calculating all jumps on the fly is rather hard (I think).