加载失败
Vera 是一个主打“让机器来写”的编程语言项目，核心想法是把变量名改成类似 De Bruijn indices（一种用位置索引代替变量名的表示法）的结构化引用，例如 @Int.0 这种写法。项目方在 FAQ 里引用了一些研究，认为大模型容易在命名上犯错，因此希望通过更少的命名、更多的类型检查和能力证明，让 LLM coding agents（基于大模型的代码代理）更容易生成可信代码。评论区把讨论扩展到语言设计：有人认为 Go（一个强调简单性的静态类型语言）这类“页面上信息更显式”的语言更适合模型，也有人希望结合 effect types（效应类型系统）、Linear Types（线性类型）、Refinement Types（细化类型）和 Unison（一个以 content addressability 为核心的语言/系统）之类的机制。整场争论其实是在问：为了迎合 LLM，编程语言应该减少语义负担，还是应该保留人类熟悉的命名和可检索性。
很多人直接反对把变量名拿掉，认为变量名本来就是把语义直接暴露给人和模型的关键线索。像 @Int.0 这种按栈位置引用，会要求一直追踪当前第几个绑定，一旦在函数前面插入新变量，后面的引用就可能连锁重排。评论里还指出，这种写法会让 grep、代码审查和局部修改都变得更难。几位评论者也强调，在复杂业务逻辑里，清晰、详细的命名和注释通常更能帮助 LLM 保持上下文。
另一类评论认为，LLM 更适合那种“页面上信息就够用”的语言。Go 和 Java 常被拿来举例：它们的语义更直接、隐藏状态更少，所以模型更容易产出可用代码；相比之下，Haskell、Erlang 这类更依赖心智模型的语言被认为更难。有人补充说，功能上更密集的语言未必更好，因为密度既能节省 context，也会让模型需要处理更多抽象。还有人提出理想方向是减少 token、尽量多做 compile-time checks，并让功能尽量局部化、写在一个文件里。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6]
有评论把重点放在类型系统对 LLM 生成代码的安全价值上，尤其是 effect types（效应类型系统）。这种思路是把 IO、网络、文件系统之类的能力提前编码进类型里，让编译器在运行前就能证明一段代码能做什么、不能做什么，从而决定是否可以直接信任或必须放进 sandbox（沙箱）里。还有人提议把 Hindley Milner、Linear Types、Refinement Types、Delimited Continuations 以及 Unison 风格的 Content Addressability 组合起来，形成一门更适合 LLM 的语言。关于“division by zero is not a runtime error”这一说法，评论者则希望看到更具体的证明机制，尤其是编译器如何检查所有调用点来保证 divisor 非零。
不少评论认为，这个项目的出发点就很可疑，像是把一个 1980 年代式的“机器如何思考”的想象套到了今天的 LLM coding agents 上。有人直接指出，它的依据看起来建立在 2023 年的研究上，和现在 agent 式编程的实际经验脱节。也有人认为，让模型去学一门完全陌生的新语言，反而违背了 LLM 的长处：它们更擅长写训练集中已经很常见的语言，而不是每次都得把语言手册和大量示例塞进 prompt。围绕 FAQ 里的论证，质疑集中在一个点上：如果要优化的是机器写代码，不代表要牺牲人类可读性和现有工具链。
有评论者明确喜欢 README 里的 “Why” 小节，认为这个项目至少把动机写得比较直接。与此同时，像“division by zero is not a runtime error”这样的表述也吸引了注意，但读者明显希望它被展开成更可验证的规则，而不是一句口号。整体上，这说明项目的概念足够新鲜，能引起兴趣，但其形式化主张仍需要更清楚的解释和例子。
De Bruijn indices: 一种用整数位置而不是变量名表示绑定变量的方式，能减少命名歧义，但可读性和检索性更差。
effect type system: 把 IO、网络、文件系统等副作用编码进类型系统，用于在编译期约束程序能做什么。
capability proof: 通过类型或编译器证明某段代码拥有或不拥有某种能力，例如不能访问网络。
Linear Types: 要求值被使用恰好一次的类型机制，常用于资源管理和避免重复使用。
Refinement Types: 在普通类型上加逻辑约束，例如要求一个整数必须非零。
Hindley Milner: 经典的多态类型推导体系，常见于 ML 家族语言。
Delimited Continuations: 一种可局部捕获和恢复控制流的机制，常用于表达复杂 effect。
Content Addressability: 用内容哈希而不是名字或路径来标识代码与文档，便于追踪和替换。