就技术来说,鸿蒙OS到底是个什么层面的东西?


#43

http://www.nuprl.org/crash/introextended.php

毕竟是 DARPA 的东西,不知道很正常。


#44

我只听说过形式化验证这个词,是不是与形式化需求对应的概念, 用数学原理写的软件需求?


#45

这个讲的不是分布式系统吗?哪里有实现 OS Kernel?

DARPA 的我只听说过 seL4 。


#46

这个项目和 seL4 是 conjuncted project。首先这个分布式系统的 spec 包括内核,其次这个项目目的是 derive specification 而不是证明已有的某个软件有什么特性,意思就是只要是符合这个 spec 的就具有 attack tolerant 的特性。


#47

一种是需求,是还没写之前倒腾出来的,另一种是验证,写完了搞证明,实践中有两种结合起来的,尤其是在具有 dependent type 的语言中。

另外其实不是数学是逻辑。当然数论在证明程序的使用也很常见。


#48

啥是CL + ML啊?


#49

这个项目也是开源的吗?关于内核部分的Spec在哪可以看到?


#50

是内部项目,完整的源码没有的,只有 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 也能做。


#51

Common Lisp — 编写 NuPRL 的主要语言

Classical ML — NuPRL 中写证明用的语言 (不同于 SML)


#52

Classical ML 和 SML有啥区别呢? 支持dependent type?


#53

http://www.nuprl.org/software/eventml/KreitzandRahli-ClassicML.pdf

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 不同的另外一种语法。


#54

你觉得haskell和ocaml哪个好

如果haskell好 但好像coq更流行

如果ocaml好 但haskell学的人更多

我就知道这么多


#55

我能不能这么理解 (Correct me if I am wrong):

LCF 是一个用 ML 写的定理证明器(本质上类似一个库),数学家使用这个库提供的组件搭建 “命题表达式” 和 “Tactic表达式”(元语言仍是 ML )?

换句话说,LCF 并不像 Idris 等 dependent type 语言(直接使用 Idris 语言本身来写 evidence),LCF 也没有提供一套自己的证明语言,而是完全使用ML(类似于embedded DSL)?


#56

唉,看来我这辈子就不指望了⋯⋯


#57

LCF 是用 Lisp 写的,设计了具有 HM type 的 ML 作为交互语言。tactics 不是表达式,而是搜索证明用的算法。

Dependent type 是啥,通常就是 type theory, type theory 通常就是 MLTT,MLTT 是不同于 LCF HOL 这类 classical logic 的 constructive logic。


#58

是否能这么理解:

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?


#59

我觉得OS的形式化验证可能有以下两个难点:

  1. 怎么验证OS的代码?

比如:假设鸿蒙的Kernel采用C语言写成(甚至混合汇编),但是C语言并不支持dependent type,你无法利用C语言的类型系统来验证程序属性。所以你必须把C语言先转化到另外一个语言上去,然后才能做证明(这里衔接的部分就是问题)。而且即使这样,由于C语言是可以写副作用的,这些副作用对reasoning并不友好。

  1. 究竟验证什么?即:如何建立模型?

比如:一个bug-free的OS究竟要满足哪些程序属性?是简单地增加前后置条件、不变量(这些条件也不是你想加就加的)?还是OS Kernel从语义上和某个数学模型等价,然后OS的一致性被规约到那个数学模型的一致性上去?


#60

哈哈,终于召唤出我大LdBeth来diss你们了image


#61

Haskell 没有 dependent type,也能用它的类型系统 CW 同构写比较 trivial 的证明。

另外有 dependent ml,是 ATS 的理论基础。

如果说写定理证明器,任何比较 sane 的语言都可以。甚至不需要语言本身有多 safe。

Constructive logic 才会用 CH 同构。


#62

所以那些声称ML擅长做定理证明的人,是否可以认为他们其实也只是 一知半解 / 人云亦云?

因为开发一个定理证明器任何语言都可以,未必一定要用ML;而如果是写Tactic,那也只是把 ML 作为脚本使用。

从语言角度并不存在什么ML擅长定理证明的说法?