写不动的类型态规约？Barista让LLM智能体代笔了

一个老问题：形式化规约太痛苦，谁来替开发者写？类型态（typestate）规约把对象生命周期和合法状态迁移编码成形式化规则——威力强大，但手写起来枯燥到让人望而却步。Barista 试图用 LLM 智能体自动合成这些规约：让智能体提议状态迁移、校验一致性、根据反馈迭代精炼。我的判断是，这是一步务实的进展——把 LLM 当脚手架而非替代品，让形式化方法走出象牙塔。但 LLM 生成的规约能否经得起真实代码库的检验，仍需硬证据。如果能，形式化方法社区就迎来了真正的自动化盟友。

原文：Barista: Synthesizing Typestate Specifications with LLM Agents · 来源：Hacker News