Vera是一种专为大型语言模型(LLM)设计的编程语言，旨在帮助LLMs编写代码。该项目托管在GitHub平台上，展示了AI代码创建领域的最新进展。

以下是GitHub仓库aallan/vera的主要内容概述：

Vera编程语言项目

1. 项目简介

• Vera是一种专为大型语言模型(LLM)设计的编程语言
• 名称源自拉丁语"veritas"(真理)
• 编译为WebAssembly，可在命令行或浏览器中运行
• 采用显式验证机制，所有函数必须声明前置条件(requires)、后置条件(ensures)和效果(effects)

2. 核心特性

• 无变量名设计：使用@Type.index结构引用(如@Int.0表示最近的Int绑定)
• 强制合约验证：编译器静态验证所有调用点
• 显式效果系统：默认纯函数，副作用需显式声明
• 详细的错误信息：包含错误代码、说明、修复示例和规范引用

3. 技术细节

• 参考编译器包含：解析器、AST、类型检查器、合约验证器(Z3)、WASM代码生成器等
• 支持代数数据类型、模式匹配、模块系统等特性
• 提供164个内置函数(字符串、数组、映射、集合、数学运算等)
• 支持JSON、HTML、Markdown、HTTP等常用功能

4. 项目状态

• 当前版本v0.0.127
• 810+提交，127次发布
• 3,638个测试，96%代码覆盖率
• 82个一致性测试程序，33个示例程序
• 13章语言规范草案

5. 设计理念

• 针对LLM的代码生成特点优化
• 强调可验证性而非正确性
• 通过结构引用减少命名相关错误
• 完整的文档系统(SKILL.md等)便于AI代理理解

6. 资源

• EXAMPLES.md：完整语言示例
• DESIGN.md：技术决策和先前工作
• HISTORY.md：编译器构建历史
• ROADMAP.md：未来发展路线

7. 使用场景

• 适合需要高可靠性的代码生成
• 可作为AI代理的目标输出语言
• 支持浏览器和命令行环境

该项目采用MIT许可证，主要依赖包括Lark(解析器)、z3-solver(验证)和wasmtime(WASM运行时)。

以下是评论内容的总结：

主要观点和论据

1. 关于变量名的争议

   • 支持保留变量名：多位评论者认为变量名对LLM生成代码至关重要，能提供语义信息，减少混淆。
     • "变量名是为了语义传达意义。这对人类写代码或LLM都重要。" (2001zhaozhao)
     • "LLM在变量和方法有明确、详细名称时更成功。" (sas41)
   • 支持去除变量名：项目设计者认为去除变量名可以减少LLM在命名上的错误。
     • "经验文献显示模型特别容易在命名相关错误上出错。" (danpalmer引用)

2. 语言设计的适用性

   • 质疑新语言的必要性：多位评论者认为LLM在已有流行语言（如JS/TS/Python）上表现更好。
     • "LLM擅长写它们训练数据中已有的语言，而不是新语言。" (DonHopkins)
     • "LLM是统计预测器，它们在TS/PY上表现最好，因为代码库更大。" (offbyone42)
   • 支持特定语言特性：部分评论者认为某些语言特性（如类型系统）对LLM有帮助。
     • "效果类型系统特别适合LLM，因为它们允许你在运行时之前精确推理程序的能力。" (unignorant)

3. 对项目实用性的质疑

   • 怀疑项目的可行性：多位评论者对项目的实际效用表示怀疑。
     • "去除变量名似乎是对LLM编码代理如何成功的基本误解。" (rtpg)
     • "为机器易于编写但人类难以阅读的编程语言不是我们需要解决的问题。" (eranation)
   • 支持设计理念：少数评论者赞同项目的某些设计理念。
     • "这里最强的想法不是语法，而是反馈循环。" (MarceliusK)

4. 其他观点

   • 语言设计建议：有评论者提出结合多种类型系统的语言设计可能更适合LLM。
     • "Hindley Milner + 线性类型 + 细化类型 + 分隔延续基于效果 + Unison风格的内容寻址将是一个很好的LLM语言。" (solomonb)
   • 对错误处理的看法：有评论者赞赏项目提供的详细错误信息。
     • "作为人类，我也更喜欢被告知出了什么问题、为什么以及如何修复，而不是expected {。" (tasuki)

总结

评论中关于变量名的作用和是否需要新语言的争议最为突出。多数评论者倾向于保留变量名和使用现有流行语言，认为这对LLM生成代码更有利。同时，对项目的实际效用和设计理念也存在较多质疑，但也有少数评论者支持项目的某些创新点。