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