所以...
我在软件工程中教授形式化方法。我还教授“敏捷方法”。大多数人似乎认为这是矛盾的。我认为这很有意义......我也在一家公司工作，我们需要真正完成工作:) 虽然我可以将我获得的技能点应用于日常的“规范”，但我的同事们通常会避开“正式”这个词。
我曾经认为这是由于我们学习编程的内在方式：我们通常被驱使寻找可行的解决方案，而不是理解问题。然后我认为这是因为正式社区中的大多数人不是工程师，而是数学家或计算机科学家。如今，我想知道是否只是因为形式方法社区隐藏在某种“混淆”法律的背后，才使用所有可用的 UNICODE 符号，积极开发粗鲁、不美观的工具，并在标准面前大笑。
是的，我一直在从“责备他们”转变为“责备我们”的观点；-)
所以，我的问题是：您在公司中使用任何形式的方法吗？你有没有介绍过它们，或者它们是先决条件？你使用什么技术来消除人们恐惧中的数学迷雾并鼓励他们使用形式化方法？您认为当前的工具缺少哪些更通用的用途？
让人们接受任何方法或方法的关键是向他们展示它如何解决他们遇到的问题。如果他们能看到这将使他们的生活变得更好，那么您就有很大的机会让他们采用这些技术。
如果你不能向他们展示这一点，也许你想采用基于哲学而不是实用性的方法。除非其他人分享您的理念，否则您将一事无成。也许你不应该。
几十年来，出现了许多方法论。新的总是解决旧的缺点，但项目仍然会遇到麻烦和失败。为什么？因为提出新方法论的摇滚明星都是摇滚明星，他们之所以提出新方法论，正是因为他们了解根本问题以及如何应用它们。那些追求的人往往会盲目地遵循食谱，而且效果并不好。
所以我认为最好的方法是教授潜在的问题，然后展示各种方法如何尝试处理这些问题。公司、项目和团队之间的差异如此之大，以至于没有一种方法可以成功地应用于所有组合。学会选择合适的工具并很好地应用它是至关重要的。
感谢您的所有贡献。他们非常有见地。请允许我发火（不过，不要把它当作私人的：-）
大多数人似乎认为形式化方法只是关于程序验证。或关键系统。如果我们追求终极的陈词滥调，这可能是正确的：证明我们正在做正确的程序（与验证相比，正如贡献者所说，它询问我们是否正在做正确的程序）。
但请考虑模型查找/检查工具，例如 Alloy。对于习惯于 UML 和 OO 的人来说，学习使用这样的工具所花费的时间可以忽略不计。不过，它可以让您立即了解您的模型。通常不超过 10 分钟就可以在一个足够小的模型子集上找到一个反例（包括首先在 Alloy 中描述模型）。
以需求工程为例。一个人通常会画很多 UML。然而，很少有人使用 OCL，而且许多业务规则都是用自然语言非正式地注释的。为什么？时间限制？
现在考虑这样一个事实，即大多数人只是用她/他的直觉来证明一个模型是可以满足的。再说一遍，为什么？我可以花同样多的时间（可能甚至更少，因为我不需要关心绘画美学）用合金写那个模型，然后只检查可满足性？我现在需要什么样的数学？“谓词”？IF 和布尔值的花哨名称 ;-) 量词？ForEachs() 的花哨名称...
大信息系统呢？它们不需要很严格......只需尝试在您的脑海中分析一个包含 600 多个类的概念（而不是实现！）图表。我看到很多人因为容易犯的模型错误而一头雾水，因为他们错过了一些约束，或者模型允许愚蠢的事情发生。
事实是，不需要从头到尾使用正式的方法。当然，我可以在 Coq 中证明整个应用程序，并证明它 100% 符合某些规范。这可能是计算机科学家/数学家的方法。
尽管如此，基于 GTD 理念，为什么我不能将一些任务委派给计算机并让它帮助改进我的开发？真的是“时间”的问题，还是单纯的缺乏技术能力和学习/创新的意愿？
在企业中进行业务线 IT 开发意味着必须将有关业务的知识从实际业务人员转移到开发人员的负责人中。虽然我自己发现抽象数学是最大的消遣之一，但它是一种糟糕的交流工具。沟通就是一切。虽然我可以想象在说服 IT 人员接受更抽象的符号方面取得了一些成功，但我基本上没有机会与业务人员打交道。
虽然在某些领域我可以看到形式化方法在企业中的作用（数学和逻辑重的专业软件，对可证明属性的重大需求，如在安全关键软件中），但它们对获得正确的要求几乎没有帮助，例如如何通过向一组可能的外部或内部供应商发出一个或多个供应订单来完成客户订单。
我认为陪审团仍然在基于模型的方法和特定领域的语言上。我认为他们的成功或失败取决于他们是否能更快地从 IT 部门向业务方面的愿望和需求提供反馈，以及他们是否认为业务人员必须进行任何重要的研究。
技术很简单。沟通很困难。正式的方法可能会帮助我们做正确的事情，但我所见过的那些方法并不能帮助我们做正确的事情。（是的，这些都是陈词滥调，但那是因为它们是不可避免且令人痛苦的真实。）
我正在上一门关于“规范和验证”的课程。作为课程结构的一部分，我们正在做以下工作- 1. PVS（原型验证系统）http://pvs.csl.sri.com/和 SMV（软件建模和验证）http://www.cs等学习工具.cmu.edu/~modelcheck/smv.html 2. 除此之外，我们还会剖析由于软件故障而发生的事故。例如 - 阿丽亚娜五世的失败
我觉得形式化的方法更适用于失败成本大于设计成本的场景。而且似乎很容易将它们用于关键系统中使用的软件。我猜它被用于航空电子、芯片设计等领域，目前的汽车行业也在将其付诸实践。
我曾几次尝试让人们接受正式的规范方法（Z 和 Alloy），并获得了与您相同的经验：大多数人虽然觉得它们有用，但在实际工作中使用它们却非常不舒服。
有趣的是，同样的人非常乐意制作大量完全无用的 UML 图。
我认为这主要有两个原因：
a.) 许多开发人员对正式方法所需的抽象级别感到不舒服。大多数入门级数学教育都是微积分和非离散数学这一事实可能与此有关。
b.) 形式化方法需要一种非常自下而上的设计方法，您从头开始设计核心模型并使其密闭，然后通过在其顶部提供接口将其连接到实际用户需求。由于我们倾向于让需求驱动开发工作，因此自上而下的方法感觉更自然，尽管它通常会导致模型不一致。这就像在你的房子已经建成之后在你的房子下面改造一个地下室。
形式化方法在失败成本低的系统中毫无意义。
在生产 Web 应用程序中，您有多个前端盒、多个后端盒、多个数据库盒 - 如果其中任何一个上的程序失败，这不是事件。硬件非常便宜，以至于您可以以远远低于正式指定所有软件的成本来构建这些系统。