Thread

1. YeGoblynQueenne · 1789739699 · focus · HN ↗

   I like it. It's like Bogosort- the Language. It would work much better if a) tokens were free and b) computation, therefore retries, didn't take any time at all. In the current world it's going to be fun watching LLMs getting stuck in infinite loops, doing and undoing their work to try and uphold a law they don't know how to uphold.

   Btw, "laws" are basically what we used to call assertions so why the new terminology?

   Edit: actually now that I think about it, it's more like constraint programming with a generate-and-test loop than assertions. Again, why not just say "constraints" instead of inventing a new term?

   1. gf000 · 1789745023 · focus · HN ↗

      It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language.

      Assertions and constraint programming is often runtime only. These languages use dependent types and verify the proves at compile time.

      1. YeGoblynQueenne · 1789763769 · focus · HN ↗

         It's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification.

         Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.

Unofficial Hacker News client; not affiliated with Y Combinator.