编译器证明让机器又写又验，人还在中间吗？

编译器写完了，谁来证明它是对的？ ICFP'26上有个演讲让我停下来看——研究者让机器自动生成编译器的正确性证明，再让另一套机器来检查。没有人在中间插手。 这听起来像是把"人写的证明"和"人审的代码"一起扔进了同一套机器流程。我的判断是：如果机器生成的证明能被同一套形式化系统验证，编译器正确性验证的瓶颈，可能就从"人写不出来"变成了"机器写得够不够对"。 但这条新闻只有1个点、0条评论。要么内容还没发酵，要么这个领域本身就安静到只有极少数人关心。我倾向于后者——形式化验证的圈层壁垒，比大多数人想象的高得多。

原文：Machine-Generated, Machine-Checked Proofs for a Verified Compiler (ICFP'26) [video] · 来源：Hacker News