我在我的编程生涯中相对较晚才了解到 Curry-Howard Isomorphism ，或许这也是我对它感到着迷的原因。它意味着每个编程概念都存在于形式逻辑中的一个精确的类比，反之亦然。以下是我能够想到的一些基本类比列表：program/definition | proof ty...

与Coq相比，Isabelle/HOL证明助手是否有任何优缺点？

继续探讨： 有没有可以证明实际可用的语言？ 我不知道你怎么看，但是我已经厌倦了编写无法保证质量的代码。 在提出以上问题并得到惊人回应后（感谢大家！），我决定将我的搜索范围缩小到一种可证明、实用、实用的方法，即Haskell。我选择 Haskell 是因为它实际上很有用（有许多Web框架用它...

看起来C语言对于在代码中使用的形式化方法具有良好的支持（frama-c、VCC、verifast）。据我所知，C++似乎没有可比较的类似支持。 有哪些形式化方法可用于推理关于采用C++编写的安全关键软件的相关问题？

这是一个有点奇怪的问题。我正在撰写一本关于使用形式化方法学习编程的书籍，目标读者是有一定编程经验的人。我的想法是教他们成为高质量的程序员。 基本符号将来自Dijkstra的Discipline of Programming，还包括一些并发和通信扩展。 与EWD不同，我希望我的学生最终能够编...

传统上，计算逻辑的大部分工作要么是命题逻辑，此时使用 SAT（布尔可满足性）求解器；要么是一阶逻辑，此时使用一阶定理证明器。 近年来，SMT（可满足性模理论）求解器取得了很多进展，基本上将命题逻辑与算术等理论结合起来；SRI国际公司的约翰•拉什比甚至称它们是一种颠覆性技术。 在一阶逻辑中可...

在使用正式方面来创建代码时，是否有一种通用的方法来确定循环不变量，还是这将完全取决于问题而有所不同？

我对形式化方法很感兴趣。我使用形式化方法来推理一些我一直在做的项目中的一些非常具体的子领域。我从未能够说服其他团队成员尝试相同的方法，更不用说使用形式化方法来指定整个领域了。 我发现特别有趣的一种方法是Alloy。我认为它可能更适合作为整个项目的基础，因为它在概念上和符号表达法上非常接近实际...

我正在尝试（经典地）证明。 ~ (forall t : U, phi) -> exists t: U, ~phi 在Coq中，我试图通过反证法来证明它： 1. Assume there is no such t (so ~(exists t: U, ~phi)) 2. Choo...

所以... 我教授软件工程中的形式化方法。我还教授“敏捷方法”。大多数人似乎认为这是矛盾的。我认为这很有道理...我还在一家公司工作，在那里我们需要实际完成任务 :) 虽然我可以在日常工作中应用我的“规范”技能，但我的同事们通常会逃避“正式”这个词。 我曾经认为这是因为我们学习编程的内在方...