请
毕竟是 DARPA 的东西，不知道很正常。
我只听说过形式化验证这个词，是不是与形式化需求对应的概念， 用数学原理写的软件需求？
这个讲的不是分布式系统吗？哪里有实现 OS Kernel？
DARPA 的我只听说过 seL4 。
这个项目和 seL4 是 conjuncted project。首先这个分布式系统的 spec 包括内核，其次这个项目目的是 derive specification 而不是证明已有的某个软件有什么特性，意思就是只要是符合这个 spec 的就具有 attack tolerant 的特性。
一种是需求，是还没写之前倒腾出来的，另一种是验证，写完了搞证明，实践中有两种结合起来的，尤其是在具有 dependent type 的语言中。
另外其实不是数学是逻辑。当然数论在证明程序的使用也很常见。
啥是CL + ML啊？
这个项目也是开源的吗？关于内核部分的Spec在哪可以看到？
是内部项目，完整的源码没有的，只有 publication 里面作为 case study 出现的 fragment。
http://www.nuprl.org/crash/publications.php
大部分都在讲 methodology。
NuPRL 和 Coq 在很多地方都是差不多的（Type System: CTT CIC 和 ITT 其实都挺像，Tactics: 都是 LCF tactics，都是 ML 系），不过 NuPRL 本身不开源用的人挺少。Coq 能做的证明原则上用 NuPRL 也能做。
Common Lisp — 编写 NuPRL 的主要语言
Classical ML — NuPRL 中写证明用的语言 （不同于 SML）
1 个赞
Classical ML 和 SML有啥区别呢？ 支持dependent type？
Classical ML 原本是 LCF 的 tactics/meta language，被 NuPRL 和 HOL88 继承了，他们都是用 Lisp 实现的，语法和 SML 差异很大，也有一些专门为证明实现的目的 SML 没有的数据类型和特性。HOL88 现在被 HOL98 取代，后者是用 SML 写的，但命题语法和 Classical ML 还是很像。
Classical ML 和 SML 一样是 HM type，因为 HOL 没有 dependent type，而 NuPRL 和 Coq 一样表示命题的是和 tactics language 不同的另外一种语法。
你觉得haskell和ocaml哪个好
如果haskell好 但好像coq更流行
如果ocaml好 但haskell学的人更多
我就知道这么多
我能不能这么理解 (Correct me if I am wrong)：
LCF 是一个用 ML 写的定理证明器（本质上类似一个库），数学家使用这个库提供的组件搭建 “命题表达式” 和 “Tactic表达式”（元语言仍是 ML ）？
换句话说，LCF 并不像 Idris 等 dependent type 语言（直接使用 Idris 语言本身来写 evidence），LCF 也没有提供一套自己的证明语言，而是完全使用ML（类似于embedded DSL）?
唉，看来我这辈子就不指望了⋯⋯
LCF 是用 Lisp 写的，设计了具有 HM type 的 ML 作为交互语言。tactics 不是表达式，而是搜索证明用的算法。
Dependent type 是啥，通常就是 type theory, type theory 通常就是 MLTT，MLTT 是不同于 LCF HOL 这类 classical logic 的 constructive logic。
是否能这么理解：
LCF对外提供了一个类似REPL的界面，这个REPL上跑的是 ML（它被当作LCF的一种脚本语言）。数学家们使用这个REPL界面来做交互式证明，写的是Tactic（比如：∃-elim、∃-intro之类的玩意，但是是用ML写）
之所以有这个疑问，是因为我常常听人说 “用ML能做定理证明”。我就纳闷了：ML又不支持dependent type，它怎么做定理证明呢？我一直以为他们描述的是用ML写定理证明器的库，然后用户通过调用这个库的接口来实现Tactic（并直接跑在ML的REPL上）。
现在从LCF作为例子来看，使用ML仅仅是因为LCF用ML作为其Tactic的脚本语言，而不是ML本身有多大能耐。。。
LCF 是不是没有使用Curry-Howard Correspondence / Propositions as Types？
我觉得OS的形式化验证可能有以下两个难点：
- 怎么验证OS的代码？
比如：假设鸿蒙的Kernel采用C语言写成(甚至混合汇编)，但是C语言并不支持dependent type，你无法利用C语言的类型系统来验证程序属性。所以你必须把C语言先转化到另外一个语言上去，然后才能做证明（这里衔接的部分就是问题）。而且即使这样，由于C语言是可以写副作用的，这些副作用对reasoning并不友好。
- 究竟验证什么？即：如何建立模型？
比如：一个bug-free的OS究竟要满足哪些程序属性？是简单地增加前后置条件、不变量（这些条件也不是你想加就加的）？还是OS Kernel从语义上和某个数学模型等价，然后OS的一致性被规约到那个数学模型的一致性上去？
1 个赞
哈哈，终于召唤出我大LdBeth来diss你们了
Haskell 没有 dependent type，也能用它的类型系统 CW 同构写比较 trivial 的证明。
另外有 dependent ml，是 ATS 的理论基础。
如果说写定理证明器，任何比较 sane 的语言都可以。甚至不需要语言本身有多 safe。
Constructive logic 才会用 CH 同构。
所以那些声称ML擅长做定理证明的人，是否可以认为他们其实也只是 一知半解 / 人云亦云？
因为开发一个定理证明器任何语言都可以，未必一定要用ML；而如果是写Tactic，那也只是把 ML 作为脚本使用。
从语言角度并不存在什么ML擅长定理证明的说法？