This part:

---

- 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: 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: https://zena-lang.dev/guide/why-zena/#familiar-to-humans-and...

along with a doc in the repo on this topic: 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.