我多年前曾从事过正确性证明的工作。[1] 我们当时拥有的证明自动化程度比许多后来的系统都要高。简单的问题被第一个SAT求解器和Oppen-Nelson简化器解决了。更难的问题则使用了Boyer-Moore定理证明器，它通过启发式方法和先前的引理来引导定理证明器。Boyer-Moore证明器需要通过建议引理来帮助它，它会尝试证明这些引理，并在后续的证明中使用它们。这就是困难的人工工作。后来的系统似乎自动化程度更低。形式化方法通常出问题的地方在于，从事这些工作的人过于沉迷于形式化。我当时是在一个商业项目中工作，希望得到无错误的代码，而不是作为学术研究。学术项目往往过于追求巧妙。它们有数学家的倾向，希望用简洁的符号表示，而很少进行案例分析。这不是一个好的解决方案。你希望有大量自动化的处理，而不需要太多洞察力。……
源讨论形式化方法与编程的未来原帖 126 条评论 · 导入时统计把你的经验，加入这段讨论。
我长期从事形式化方法的工作，我有点不同意你所说的新逻辑没有帮助的说法。工业逻辑非常实用，可以让你以非常简洁的方式写出系统应满足的各种复杂属性。逻辑对于计算机科学和软件工程的意义，就像微积分对于物理学以及机械或土木工程的意义一样[1, 2]。 TLA+已经获得了相当大的流行度，这证明了这一点。模型检测非常实用。现在令人兴奋的是，更重的形式化方法，特别是定理证明，可能变得足够便宜，可以在常规系统软件中使用。为函数编写形式化规范，并通过某种SAT/SMT、定理证明器和大型语言模型的混合方法进行综合和证明正确，可能在不久的将来成为常态。 [1] 关于逻辑的不寻常的有效性…
完整原文你有看过ADA Spark吗？ 如果你看过，它是否符合你对事情应该如何进行的直觉？ 我正在慢慢开发一些东西，希望可以整合这种能力，处理类型系统无法快速处理的事情。 因此，我对曾经走过这条路的人的观点很感兴趣。
完整原文人类的可理解性和人类的构建对于形式化规范来说将变得非常重要。 我的担忧是，我们会得到难以理解的数学内容，这些内容将被一小群信徒所保护。不同的难以理解的符号之间将互不兼容，理解其中一个并不会真正帮助理解其他。大多数人只会写出无法正确验证的英文陈述。 更糟糕的是，人们会让机器来形式化他们的陈述，但他们并不理解形式化或证明，却会参与验证的表演，并在一切崩溃时表现出震惊。
完整原文尊重不同观点，分享具体经验。
登录后即可发帖、评论、转发和引用。