拿形式化证明给 AI 写的代码兜底，听着很硬核。可我觉得最难的不在证明那一步。

微软研究院这个 PDD Kit 的流程是两步：先把开发者的意图翻译成形式化规格，再用 Verus（Rust 的验证工具）证明生成的代码满足这份规格。

麻烦在第一步。证明只能说明代码和规格对得上。规格要是把意图理解歪了，或者漏了某个边界条件，证明照样能通过，而且还会让人觉得“这段已经被证明过了”，反而更不会去细看。

帖子里说翻译规格是工具来做的。那这份规格谁来审？

目前能确定的只有支持 Rust、接进了 GitHub Next 的 Chopin，28 号 GitHub Universe 上会演示。到时候我主要看它怎么让人审规格，证明那部分我倒没那么担心。

#人工智能 #程序员 #AI编程 #Rust #微软