编译器强制验证代码契约的新语言

#ARTICLE HackerNews 2026.11.05

推荐指数 69.0 NO. 018 · 2026.11.05

发布2026/11/04Score96Comments82

简介

Evergreen 是一门将前置条件、后置条件和数据不变量直接嵌入代码的系统级语言，编译期自动验证契约而非运行时检查。对需要高可靠性的 AI 基础设施（推理引擎、分布式调度）有参考价值，能在编译阶段消灭一类内存安全和逻辑错误。

编辑判断

Rust 用所有权系统解决了内存安全，但逻辑错误（如数组越界、除零、状态机违规）仍靠运行时 panic 或开发者自觉。Evergreen 的契约式设计把这类检查推进到编译期，代价是需要形式化证明或 SMT 求解器辅助验证，编译时间会显著增加。

目前这门语言还在早期，工具链成熟度远不及 Rust。但如果你在做 AI 推理引擎或区块链节点这类一旦出错就损失巨大的系统，它的思路值得跟踪——类似的理念在 Microsoft 的 Verus 和 Golang 的 contracts 提案里也在推进，说明行业正在从内存安全向逻辑安全延伸。

社区反馈

意见分歧 61 条评论

核心争论：AI时代应优化语言给人类还是AI agent使用，契约验证语言能否替代Rust

jordan_bonecut

This language has been something I've wanted to build for years. For a while I thought I'd get my PhD and build it there. But now it's very possible to have Claude build it while I'm at work and give it intense code review every day. It's still not in a "useful" place yet, but I'm curious what fello

sblom

It's a really great concept. What guarantees are made by the prover? Success in programming languages is not simply if-you-build-it-they-will-come. Bootstrapping a community that loves programming in it is the hard part. You'll either need a killer interop story with an already built ecosystem, or y

jordan_bonecut

Thanks! The guarantee is that, without the use of trustme (which can prove any fact), you cannot address memory as the wrong type. The compiler also ensures that a pointer/reference to a value is live at compile time, so it’s not possible to create an invalid pointer (without the use of trustme

替代方案： RustKaniVerusLean

查看原文 →