idris - 强类型函数式编程语言中模型检查的相关性？

Question

我目前正在学习模型检查（模态逻辑、LTL、CTL、SAL 模型检查器等），在业余时间我正在学习 Idris，它是一种支持依赖类型的强类型函数式编程语言。由于我同时关注模型检查和 Idris，我开始对 Idris 与形式方法和模型检查的关系感到好奇。

在学习模型检查时，感觉提出的大多数示例要么是关于验证以命令式方式编写的系统，要么是关于硬件组件。因此，我对模型检查在强类型函数式编程语言中的相关性感到困惑，尤其是在 Idris 等依赖类型语言中，在我看来，类型检查器在验证正确性方面已经做得非常出色。 然而，我的直觉告诉我，模型检查可能与不提供任何终止承诺的部分函数有关。

使用 Idris 等强依赖类型编程语言时，模型检查是否相关？

Answer 1

没错，模型检查最常用于硬件验证和命令式（通常是并发）程序，因为它的起源也在这个领域。对于功能程序，复杂的类型系统技术被广泛用于验证。但是，它们通常需要大量注释，或者可能会产生“误报”，从而驳斥“正确”的程序。模型检查不需要这些注释，还可以回答更具体的问题。我不是该领域的专家，但似乎类型系统和模型检查的技术经常结合用于功能程序。如果您对功能程序模型检查的当前研究和方法感兴趣，有一个很好的课程，在线提供大量材料：

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

该课程由该领域的主要研究人员之一 Luke Ong 准备。