3 ms·

I'm still waiting to see the first show HN I made a language designed for LLMs to write programs better.

• mickael-kerjean 7mo ago
  It came up a few weeks ago already, can't find the link
• fourthark 7mo ago
  There have been a few.
• fcatalan 7mo ago
  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 7mo ago
    If you don't mind, could you drop some code? I'd be interested to see the result :)
    • fcatalan 7mo ago
      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 7mo ago
        How does it do the proving?
        • fcatalan 7mo ago
          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 7mo ago
            thanks.
  • ryanmcl 7mo ago
    [dead]
    • fcatalan 7mo ago
      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.
    • presbyterian 7mo ago
      > 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.
    • dev_l1x_be 7mo ago
      If you want to go really meta ask Claude Code to re-implement itself in the new language. You could keep going doing this.
      • fcatalan 7mo ago
        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...