[fcatalan]

A few days ago I asked Claude what kind of language it would like to program in, and it said something like Forth but with static typing, contracts, and constraint solving, implemented on the Erlang BEAM.

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.

[alexisread]

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

[fcatalan]

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

[fuzztester]

How does it do the proving?

[fcatalan]

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 :)

[fuzztester]

thanks.