> Token density

If you really cared about that, you wouldn't have picked Rust. Nim or Haskell are terser languages.

> Every language we’ve built defaults to sequential execution with parallelism bolted on.

False and misleading statement. Array languages have been around for a long time, but you didn't care to learn them.

> Formal verifiability. Move beyond type checking to compile-time proofs.

Good luck with your tokens budget for proof providing. LLMs won't solve that for you. If you believe that proofs are as simple as matching API calling inerfaces you're wrong.

> Declared effects. Every function explicitly states what it reads, writes, and depends on, machine-enforced.

Good functions are pure functions that have no effects. Good design tries to minimize the number of effects needed and maximize the footprint of pure functions mapped over inputs and outputs. If you insist that every function needs an explicit effect annotation, you don't know the topic and you haven't worked with effect systems much.