Vera is a new language targeting LLM code generation: no variable names, mandatory contracts verified by Z3, typed effects, compiles to WebAssembly.
Key Takeaways
Uses typed De Bruijn slot references (@Int.0, @Int.1) instead of variable names to eliminate naming-related errors LLMs commonly make.
Every function requires requires(), ensures(), and effects() clauses; Z3 proves Tier 1 contracts statically, with runtime fallback for undecidable cases.
Algebraic effects (<IO>, <Http>, <Inference>, <State>) are tracked in the type system, so callers must explicitly declare any side-effectful capability.
Compiler diagnostics are structured as agent instructions with stable error codes (E001-E702) and --json output designed for agent feedback loops.
VeraBench results show Kimi K2.5 achieves 100% run_correct on Vera vs 86% Python; three models beat TypeScript on Vera, though results are single-run with high variance.
Hacker News Comment Review
Core skepticism centers on the no-names design: commenters argue LLMs succeed when more is explicit in text, not less, and that verbose structural references may hurt rather than help token prediction.
Several commenters note LLM coding ability tracks corpus size, pointing to Python/TypeScript dominance over Haskell as evidence that novel syntax will hit a cold-start problem regardless of formal properties.
A counter-thread sees real value in effect type systems specifically for agent sandboxing: capability proofs at compile time let you verify agent-written code cannot do IO before running it.
Notable Comments
@solomonb: proposes Hindley-Milner + Linear Types + Refinement Types + Delimited Continuation Effects + Unison-style content addressability as a more principled LLM-friendly stack.
@unignorant: highlights effect type systems as a strong fit for agent trust: “you know it can’t do IO” before runtime.
