加载失败
CodeSpeak（标题所指的项目）把 Markdown 风格的“规格”当作工程的第一阶产物，提供 `codespeak build`（从规格用 LLM 生成代码）与 `codespeak takeover`（从代码反向生成规格）等命令，宣称把规格作为源头以便长期维护。社区讨论围绕三个主轴展开：一是这到底是“新语言”还是仅仅把规格作为工作流层的工具；二是 LLM 输出的非确定性与大规模形式化验证的可行性问题；三是工程上可行的折中方案，包括从规格生成测试（如 PBT/Hypothesis）、混合模式的增量变更以及为 agents 管理上下文与知识。评论中还引用了既有工具（Kiro IDE、EARS/INCOSE 格式、TLA+ 等）与历史争论（如 Joel Spolsky 的观点），并提出了关于闭源、供应商依赖与可替代性等商业与生态层面的担忧。
许多评论把 CodeSpeak 当成一种工作流或工具，而不是传统意义上的新语言：开发者把功能用 Markdown 风格的规格文件写清，`codespeak build` 根据规格调用 LLM 生成代码，`codespeak takeover` 可以把已有文件反向生成规格并支持混合模式（只触及允许的文件）。优点包括将 prompts 与规格一并保存、把规格差异映射为代码差异以便审查、以及在项目早期快速生成可评审实现。现实限制也被多次指出：当前实现对 agent 配置有限、依赖第三方模型 API（例：Anthropic），并可能导致手工修改与规格不同步或遗漏隐含行为。
反对者认为把规格当“源码”有根本性问题：写出一个足以自动生成正确程序的完整规格，实际上与直接写代码一样困难，早期批评（如 Joel Spolsky 的论点）在社区中被反复引用。更重要的是 LLM 在“填空”时表现出非确定性——模型会根据种子、temperature、实现细节或上下文产生不同实现，规格不能消除这种不稳定性。形式化验证被提出来作为可能的解决方案，但评论里有人以理论与实践例子（如对复杂性的讨论和少数已验证项目）说明大规模、全面的形式化证明在成本和可行性上都很难推广。总体结论是：规格并不自动等价于可证明正确或更易维护的代码。
很多评论提出务实路线：把规格先转成测试（包括 property-based tests），再用红绿 TDD 循环把测试变绿，从测试来断定实现是否满足规格。有人提到 Kiro IDE 会以 EARS/INCOSE（工程需求格式）生成规格并导出 Hypothesis（Python 的 PBT）测试，另有实践者把测试与规格条目一一关联，并在 CI 中强制运行以避免漂移。混合模式也被反复建议：允许对特定文件手工修补并要求代理对现有实现做增量修改而非整仓重写，从而在自动化与人工干预间取得可控权衡。
若把這類工作流當作商業產品出售，评论里有人怀疑其可持续性：闭源实现易被社区复刻为开源替代品，且依赖外部模型与登录/API（例如 Anthropic 的 key）会带来供应商锁定与可替换性问题。有人直言该类想法技术门槛低、能在短时间内被重实现，因此难以形成长期付费护城河。对标题用词（如“formal”或“编程语言”）的夸张宣传也被认为会误导用户。
另一组评论把焦点放在上下文与知识而非语法：即便规范书写完整，模型仍可能缺乏产品的隐含边界、历史决策或“部落知识”，有评论把这类可由模型自行覆盖的领域称为 "esoteric knowledge ratio" 仅约 40–55%。模型对仓库级上下文、记忆和文件格式的理解常决定结果质量；因此有人建议优先改进知识结构化、上下文注入与 agent 的长期记忆，而不是只纠结在一种新式的规范语法上。讨论也涉及到为 LLM 优化的文件格式与按任务计 token 成本的工程化做法。
规格驱动开发（Spec-driven development, SDD）: 以人可读的规格（常为 Markdown）作为源头，规范描述软件应有的行为并由 LLM 将这些规格转为代码，强调把决策与 prompts 同步保存在仓库中以便审查和回滚。
Agent / agentic engineering: 由多步提示链、工具调用与任务调度组成的自动化 LLM 代理体系（agents），可在 CLI 或 tmux 等环境中以脚本化方式执行实现、测试与变更。
非确定性（Determinism of LLM outputs）: 指相同输入下模型输出可能不同的现象，成因包括 temperature、seed、批处理、并行实现与服务端策略；讨论中还涉及是否以测试/规范来替代对底层确定性的需求。
属性测试（Property-based testing, PBT） / Hypothesis: 通过对输入域进行广泛生成与断言性质来发现边界问题的测试方法，评论中提到用 Hypothesis 为由规格生成的实现自动构造大量测试以提高置信度。
形式规范与形式化验证（Formal specification & verification; 例：TLA+, Lean, Dafny, Coq, CompCert, seL4）: 用数学或逻辑语言精确描述系统并以证明或模型检验方式验证实现符合规范；讨论指出这类验证对大型工程通常成本极高，仅在少数关键项目中完成过全量证明。
BDD / Gherkin: 行为驱动开发（Behavior Driven Development）的一种可读规范语法（如 Gherkin），常用于把接受测试以类似自然语言的形式写成机器可处理的场景。