- Correct by construction: the language makes invalid states or programs hard or impossible to express.
- Statically established: types, proofs, and static analysis establish properties before execution.
- Runtime-enforced: memory management, isolation, capability boundaries, and other runtime enforced properties.
- Empirically validated: program validation through tests, property-based testing, and fuzzing.
---
Along with being familiar, so it's easy to generate, is a huge part of why I'm building Zena: <a href="https://zena-lang.dev/" rel="nofollow">https://zena-lang.dev/
I don't have the AI-first rationale put into the public docs well just yet, but I mention some of it here: <a href="https://zena-lang.dev/guide/why-zena/#familiar-to-humans-and-to-agents" rel="nofollow">https://zena-lang.dev/guide/why-zena/#familiar-to-humans-and...
along with a doc in the repo on this topic: <a href="https://github.com/elematic/zena/blob/main/docs/design/ai-first-language.md" rel="nofollow">https://github.com/elematic/zena/blob/main/docs/design/ai-fi...
In short, the more deterministic, automated, checks the better. AI can deal with a pedantic language. I intend to add statically verified structured concurrency, units of measure, contracts, and eventually more and more formal methods into the language so it can be a familiar TYpeScript-like base with as many static guarantees as we can fit in.
I also think that fine-grained isolation, which Zena gets via Web Assembly, is critical for limiting the capabilities of generated code and the blast radius of bugs, vulnerabilities, and non-aligned behavior.
I do have an optimistic hope that a language also optimized for humans, readability and simple semantics especially, has value in the future, even when most code is generated. We'll see about that.
> bc agents will naturally be bad at it due to a lack of examples.
Can we please as a community stop parroting these false premises as a basis of every argument against doing anything new? It's plainly obvious to anybody that uses LLMs on a regular basis that it's not true.
It might seem obvious but in truth is not - to be honest, a strictly typed language where models can play adversarial competitions against a strict compiler/linter does have advantages, as mentioned in the article itself but that's not related to training size, the advantage is exactly that it can generate synthetic useful data due to compiler/linter guarantees - regarding training size as long as some logic showcasing the constructs exists that is all that is needed. If you have 2 correct examples for each feature or language construct then the probability of the a LLM learning it and applying it is very much guaranteed, if you have thousands of diverging uses of patterns and constructs in the training data (with a lot of bad examples or wrong uses) a LLM might, I dare say will, actually perform worse, since the probabilities of what particular variation being the "correct" one to use are all over the place.
What can happen is sometimes patterns that are unique to certain languages aren't surfaced and so can't be "learned" but that is a different case, since you can add examples - or patterns that go beyond syntax (threaded code, process isolation, interaction between different modes of resolution, etc) where you need the agent to be able to understand and plan higher-level logic.
I wrote CSSex as a css pre-processor (similar but not the same as SASS/SCSS) and my "boss" at the time fed the existing cssex files to GPT (+2 years ago) and it was able to write CSSex just as fine as if it was writing something that was present in its training data set. It never introduced syntax bugs, the bugs it introduced were all relative to complex cascading styles rules in an existing large (for a definition of large in webapps) codebase, rules interactions (CSS), browser quirks, and complex logic to do what we "humans" wanted (or him in this case) and so on.
spankalee · · focus · HN ↗
---
- Correct by construction: the language makes invalid states or programs hard or impossible to express.
- Statically established: types, proofs, and static analysis establish properties before execution.
- Runtime-enforced: memory management, isolation, capability boundaries, and other runtime enforced properties.
- Empirically validated: program validation through tests, property-based testing, and fuzzing.
---
Along with being familiar, so it's easy to generate, is a huge part of why I'm building Zena: <a href="https://zena-lang.dev/" rel="nofollow">https://zena-lang.dev/
I don't have the AI-first rationale put into the public docs well just yet, but I mention some of it here: <a href="https://zena-lang.dev/guide/why-zena/#familiar-to-humans-and-to-agents" rel="nofollow">https://zena-lang.dev/guide/why-zena/#familiar-to-humans-and...
along with a doc in the repo on this topic: <a href="https://github.com/elematic/zena/blob/main/docs/design/ai-first-language.md" rel="nofollow">https://github.com/elematic/zena/blob/main/docs/design/ai-fi...
In short, the more deterministic, automated, checks the better. AI can deal with a pedantic language. I intend to add statically verified structured concurrency, units of measure, contracts, and eventually more and more formal methods into the language so it can be a familiar TYpeScript-like base with as many static guarantees as we can fit in.
I also think that fine-grained isolation, which Zena gets via Web Assembly, is critical for limiting the capabilities of generated code and the blast radius of bugs, vulnerabilities, and non-aligned behavior.
I do have an optimistic hope that a language also optimized for humans, readability and simple semantics especially, has value in the future, even when most code is generated. We'll see about that.
demibabs · · focus · HN ↗
Agents will naturally be bad at it due to a lack of examples.
abletonlive · · focus · HN ↗
Can we please as a community stop parroting these false premises as a basis of every argument against doing anything new? It's plainly obvious to anybody that uses LLMs on a regular basis that it's not true.
demibabs · · focus · HN ↗
hnedeotes · · focus · HN ↗
What can happen is sometimes patterns that are unique to certain languages aren't surfaced and so can't be "learned" but that is a different case, since you can add examples - or patterns that go beyond syntax (threaded code, process isolation, interaction between different modes of resolution, etc) where you need the agent to be able to understand and plan higher-level logic.
I wrote CSSex as a css pre-processor (similar but not the same as SASS/SCSS) and my "boss" at the time fed the existing cssex files to GPT (+2 years ago) and it was able to write CSSex just as fine as if it was writing something that was present in its training data set. It never introduced syntax bugs, the bugs it introduced were all relative to complex cascading styles rules in an existing large (for a definition of large in webapps) codebase, rules interactions (CSS), browser quirks, and complex logic to do what we "humans" wanted (or him in this case) and so on.