专题：formal-specification

探讨LLM生成代码的局限性，区分规范与代码的抽象本质。通过英里转公里案例说明规范的多义性，指出程序合成仍是研究领域，强调测试用例作为规范的实践价值。核心观点：规范是实现的约束条件，而非具体代码，程序员仍需参与规范抽象过程。